The structure of exponentials: Uncovering the dynamics of linear logic proofs

AbstractWe exhibit the cartesian differential categories of Blute, Cockett and Seely as a particular kind of enriched category. The base for the enrichment is the category of commutative monoids—or in a straightforward generalisation, the category of modules over a commutative rig k. However, the tensor product on this category is not the usual one, but rather a warping of it by a certain monoidal comonad Q. Thus the enrichment base is not a monoidal category in the usual sense, but rather a skew monoidal category in the sense of Szlachányi. Our first main result is that cartesian differential categories are the same as categories with finite products enriched over this skew monoidal base. The comonad Q involved is, in fact, an example of a differential modality. Differential modalities are a kind of comonad on a symmetric monoidal k-linear category with the characteristic feature that their co-Kleisli categories are cartesian differential categories. Using our first main result, we are able to prove our second one: that every small cartesian differential category admits a full, structure-preserving embedding into the cartesian differential category induced by a differential modality (in fact, a monoidal differential modality on a monoidal closed category—thus, a model of intuitionistic differential linear logic). This resolves an important open question in this area.

Download Full-text

Type inference in intuitionistic linear logic

Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming - PPDP '10 ◽

10.1145/1836089.1836118 ◽

2010 ◽

Cited By ~ 4

Author(s):

Patrick Baillot ◽

Martin Hofmann

Keyword(s):

Linear Logic ◽

Type Inference ◽

Intuitionistic Linear Logic

Download Full-text

On Polymorphic Sessions and Functions

ACM Transactions on Programming Languages and Systems ◽

10.1145/3457884 ◽

2021 ◽

Vol 43 (2) ◽

pp. 1-55

Author(s):

Bernardo Toninho ◽

Nobuko Yoshida

Keyword(s):

Natural Deduction ◽

Sequent Calculus ◽

Linear Logic ◽

Linear Formulation ◽

Session Types ◽

Logical Foundation ◽

Π Calculus ◽

Soundness And Completeness ◽

System F ◽

Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Download Full-text