Linear logic is an example of a "resource-sensitive" logic, keeping track of the number of times data of given types are used. Formulas in linear logic represent either the data themselves or data types, whereas in ordinary logic a formula is a proposition. If ordinary logic is a logic of truth, linear logic is a logic of actions.
Linear logic and its implications are explored in depth in this volume. Particular attention has been given to the various formalisms for linear logic, embeddings of classical and intuitionistic logic into linear logic, the connection with certain types of categories, the "formulas-as-types" paradigm for linear logic and associated computational interpretations, and Girard's proof nets for classical linear logic as an analogue of natural deduction. It is also shown that linear logic is undecidable. A final section, contributed by D. Roorda, presents a proof of strong normalization for cut elimination in linear logic.
Linear logic is of interest to logicians and computer scientists, and shows links with many other topics, such as coherence theorems in category theory, the theory of Petri nets, and abstract computing machines without garbage collection.
is professor emeritus of pure mathematics and foundations of mathematics at the Institute of Logic, Language, and Information (ILLC) of the University of Amsterdam.
- 1 Introduction
- 2 Sequent calculus for linear logic
- 3 Some elementary syntactic results
- 4 The calculus of two implications
- 5 Embeddings and approximations
- 6 Natural deduction systems for linear logic
- 7 Hillbert-type systemens
- 8 Algebraic semantics
- 9 Combinational linear logic
- 10 Girard domains
- 11 Coherence in symmetric monoidal
- 12 The storage operator as a cofree comonoid
- 13 Evaluation in typed calculii
- 14 Computation by lazy evaluation in CCC's
- 15 Computation by lazy evaluation in SMC's and ILC's
- 17 The categorical and linear machine
- 18 Proofnets for the multiplicative fragment
- 19 The algorithm of cut elimination for proof nets
- 20 The undecidability of linear logic
- 21 Cut elimination and strong normalization