CR: Logical Foundations of Programming Languages (2020-2021)
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.
Taking advantage of the organisation of the semester in two waves, we
plan to cover the following two tracks in parallel.
- Sequent calculus for classical and intuitionistic logics
- Classical and intuitionistic linear logic
- Proof nets
- Symmetric monoidal closed categories
- The relational model
- 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.
(To be confirmed)
Homeworks (1/2) + presentation (and short report) on a research article (1/2).