CR03: Logical Foundations of Programming Languages (2021-2022)

Description

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.

Teachers

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

Practical informations

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

Content

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

Preliminary Content

Taking advantage of the organisation of the semester in two waves, we plan to cover the following two tracks in parallel.

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

Prerequisites

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

References

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)

Evaluation

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