Lectures on Linear Logic

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.