# CR: Logical Foundations of Programming Languages (2020-2021)

## 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

## 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

## Evaluation

*(To be confirmed)*

Homeworks (1/2) + presentation (and short report) on a research article (1/2).