Linear logic

Table 1: Important variants of linear logic and their categorical semantics
Name Connectives Categorical semantics
Multiplicative linear logic without negation \(\otimes\), \(⅋\), \(1\), \(\bot\) Linearly distributive categories
Multiplicative linear logic (MLL) \(\otimes\), \(⅋\), \(1\), \(\bot\), \((-)^\bot\) *-autonomous categories
Multiplicative intuitionistic linear logic (MILL) \(\otimes\), \(1\), \(\multimap\) Closed monoidal categories
(Classical) linear logic \(\&\), \(\oplus\), \(\top\), \(0\), \(\otimes\), \(⅋\), \(1\), \(\bot\), \((-)^\bot\), \(!\), \(?\)  

The nLab lists more variants of linear logic.

Logical system of linear logic

Linear logic is a logical system invented by Jean-Yves Girard:

  • Girard, 1987: Linear logic (doi)
    • Seminal paper introducing linear logic and proof nets
  • Girard, 1995: Linear logic: its syntax and semantics (pdf)

Girard has also exposited linear logic in his books, in his distinctive (sometimes incomprehensible) style:

  • Girard, 1989: Proofs and Types (pdf), Appendix B: What is linear logic?
    • Appendix B is actually written by Yves Lafont
  • Girard, 2011: Lectures on Logic (doi), Part III: Linear logic

By now there are many surveys of linear logic, written from different perspectives:

  • For logicians:
    • Di Cosmo, 1996: Introduction to linear logic (pdf)
    • Earlier version with Danos appeared as “The linear logic primer” (pdf)
  • For proof theorists:
    • Troelstra, 1992, via CSLI: Lectures on linear logic
    • Troelstra & Schwichtenberg, 2000: Basic proof theory, Ch. 9: Modal and linear logic (doi)
  • For philosophers: Di Cosmo & Miller, 2006, in SEP: Linear logic
  • For programming language theorists:
    • Wadler, 1993: A taste of linear logic (doi, pdf)
    • Wadler, 1990: Linear types can change the world! (ps )
    • Walker, 2002: Substructural type systems (Ch 1. in Pierce’s Advanced Topics in Types and Programming Languages)
  • For linguists: Crouch & Genabith, 2000: Linear logic for linguists (pdf)
  • For category theorists: see “categorical semantics” below
  • For algebraists: Murfet, 2014: Logic and linear algebra: an introduction (arxiv)

Categorical semantics of linear logic

Several surveys aim to present a holistic view of linear logic’s categorical semantics:

  • Schalk, 2004: What is a categorical model for linear logic? (pdf)
  • Mellies, 2006: Categorical semantics of linear logic: A survey (pdf)
    • Earlier, even longer version with extra two chapters (pdf)
    • Mellies, 2003: Categorical models of linear logic revisited (pdf)
  • de Paiva, 2014: Categorical semantics of linear logic for all (doi, pdf)

The main references for linearly distributive categories are the original papers by Hyland & de Paiva and by Cockett and Seely. Linearly distributive categories were originally called “weakly distributive categories” because, although they do not weaken classical distributivity in the obvious way that rig categories do, a cartesian monoidal category that is weakly distribtive is classically distributive.

  • Hyland & de Paiva, 1993: Full intuitionistic linear logic (extended abstract) (doi)
  • Benton, Bierman, de Paiva, Hyland, 1993: A term calculus for intuitionistic linear logic (doi, pdf)
    • Sec 8 of longer tech report treats categorical semantics (doi, pdf)
  • Cockett & Seely, 1997: Weakly distributive categories (doi)
    • Conference version in 1992 (doi)
  • Cockett & Seely, 1999: Linearly distributive functors (doi)
  • Blute, Cockett, Seely, Trimble, 1996: Natural deduction and coherence for weakly distributive categories (doi)
    • Introduces a graphical language for Girard’s proof nets reminiscent of string diagrams
    • Language rules are quite complicated due to presence of units