The objective of this course is to present the three sides of the Curry-Howard-Lambek correspondence between proofs, programs and denotational semantics, with an emphasis on the proof-theoretical insights provided by Linear Logic.

- Olivier Laurent (Monday 10:15am - 12:15pm, starts 2021/09/13)
- Colin Riba (Thursday 3:45pm - 5:45pm, starts 2021/09/09)

- room B1
**FINAL EXAM : Friday November, 12th, 2:00pm - 5:00pm**

- Programs part (Thursday, Colin Riba)
- Proofs part (Monday, Olivier Laurent)

- Proofs
- Sequent calculus for classical and intuitionistic logics
- Classical and intuitionistic linear logic
- Proof nets
- Symmetric monoidal closed categories
- The relational model

- Programs
- Gödel's System T
- The language PCF
- Girard's System F
- Cartesian closed categories
- Intersection types

We shall assume some basic familiarity with natural deduction and (simply) typed lambda-calculus.

- Interactive tutorial on sequent calculus
- Interactive linear logic sequent calculus prover
- Proofs and Types
*(introduction to proof theory and λ-calculus)* - Théorie de la démonstration / Proof Theory
*(course notes in French)* - Proof Nets
*(course notes)* - LL Wiki
*(wiki on Linear Logic)*

Homeworks O. Laurent (1/4) + Homeworks C. Riba (1/4) + Exam (1/2).