Lectures on linear logic

This chapter discusses Sequent calculus for linear logic, the calculus of two implications: a digression and the algorithm of cut elimination for proof nets.

Abstract

1. Introduction 2. Sequent calculus for linear logic 3. Some elementary syntactic results 4. The calculus of two implications: a digression 5. Embeddings and approximations 6. Natural deduction systems for linear logic 7. Hilbert-type systems 8. Algebraic semantics 9. Combinatorial linear logic 10. Girard domains 11. Coherence in symmetric monoidal categories 12. The storage operator as a coffee comonoid 13. Evaluation in typed calculi 14. Computation by lazy evaluation in CCC's 15. Computation by lazy evaluation in SMC's and ILC's 16. The categorical and linear machine 17. Proofnets for the multiplicative fragment 18. The algorithm of cut elimination for proof nets 19. Multiplicative operators 20. The undecidability of linear logic 21. Cut elimination and strong normalization References Index.