CR 17: 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

Practical informations

Content

Preliminary Content

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

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).