ABSTRACT. In this paper, we investigate how to introduce dependent types into the substructural calculi such as the Lambek calculus and linear logic. The motivations of such a move include facilitating a closer correspondence between syntax and semantics in natural language analysis and developing promising applications such as that to concurrency through dependent session types.

We shall present two substructural calculi with dependent types: the first containing dependent Lambek types and the second dependent linear types. Technically, the former adheres to the usual assumption that types do not depend on substructural variables (in this case, the Lambek variables), which makes the technical development easier, while the latter allows type dependency on linear variables, which makes the development more challenging as well as more interesting in applications.

ABSTRACT. In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton’s Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.

ABSTRACT. We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the Bang Calculus, a paradigmatic functional language with an explicit box-operator that allows both the call-by-name and call-by value lambda-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value lambda-calculi from both a syntactic and a semantic point of view.

ABSTRACT. Process calculi based in logic, such as πDill and CP, provide a foundation for deadlock-free concurrent programming. However, there is a mismatch between the structures of operators used as proof terms in previous work, and the term constructs of the standard π-calculus. We introduce the Hypersequent Classical Processes (HCP), which addresses this mismatch. The key insight is to register parallelism in the typing judgements using hypersequents, a technique from logic which generalises judgements from one sequent to many. This allows us to take apart the term constructs used in Classical Processes (CP) to more closely match those of the standard π-calculus. We prove that HCP enjoys subject reduction and progress, and prove several properties relating it back to CP.

ABSTRACT. This paper studies the so-called generalized multiplicative connectives of linear logic, focusing on the question of finding the ``non-decomposable'' ones, i.e., those that may not be expressed as combinations of the default binary connectives of multiplicative linear logic, Tensor and Par. In particular, we concentrate on generalized connectives of a surprisingly simple form, called ``entangled connectives'', and prove a characterization theorem giving a criterion for identifying the decomposable (resp., undecomposable) entangled connectives.

ABSTRACT. We show that the normal form of the Taylor expansion of a λ-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier’s original proof along three independent directions.

First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad-hoc.

We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables.

Finally, we extend all the results to a non-deterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier’s approach can be preserved in this setting.

ABSTRACT. We present a translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing. This translation is derived from a simple observation on the Int-construction on traced monoidal categories. It turns out that the translation is a mixture of the call-by-name CPS translation and the Geometry of Interaction-based interpretation.

ABSTRACT. Proof nets provide permutation-independent representations of proofs and are used to investigate coherence problems for monoidal categories. We investigate a coherence problem concerning Second Order Multiplicative Linear Logic MLL2, that is, the one of characterizing the equivalence over proofs generated by the interpretation of quantifiers by means of ends and coends. By adapting the "rewiring approach" used in the proof net characterization of the free *-autonomous category, we provide a compact representation of proof nets for a fragment of MLL2 related to the Yoneda isomorphism. We prove that the equivalence generated by coends over proofs in this fragment is fully characterized by the rewiring equivalence over proof nets.

ABSTRACT. We introduce the functional language IQu which, under the paradigm “quantum data & classical control” and in accordance with the model QRAM, allows to define and manipulate quantum circuits and quantum states on which we can execute partial measurement. IQu tailors a lot of ideas from the design of Idealized Algol (roughly, PCF extended with local stores and assignment) and its side-effect management. These ideas play a crucial role in the language design: each quantum co-processor is formalized by means of a quantum register (storing a quantum state) that can be modified by quantum directives (lists of unitary gates). The linearity of quantum states is assured by a one-to one correspondence between quantum states and quantum registers. We adapt the type system of Idealized Algol for typing both quantum-registers and quantum-directives. The types for quantum registers are parametric on the number of qubits and their linearity is granted for free. IQu operates on quantum circuits as they were classical data so no restriction exists on their duplication.