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 (Thursday 1:30pm - 3:30pm)
- Colin Riba (Wednesday 8:00am - 10:00am)

- The course will be partly physical and partly remote.
- The physical part is in room B1.
- The remote part will use BBB.
- Groups for physical vs. remote are on the pad.
- Connection informations for remote attendance are on the pad.

- Programs part (Wednesday, Colin Riba)
- Proofs part (Thursday, 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
- Proofs and Types
*(introduction to proof theory and λ-calculus)* - Théorie de la démonstration / Proof Theory
*(course notes in French)* - LL Wiki
*(wiki on Linear Logic)*

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