Curry-Howard correspondence for Classical Logic
MPRI

For any question, do not hesitate to write to Stephane.Lengrand[AT]Polytechnique.edu
All lectures in one file: pdf

Lecture 1: Classical Logic as a typing system
overlays
without overlay

Lecture 2: Non-confluence, strong normalisation, and orthogonality
overlays
without overlay

Lecture 3: Recovering confluence: the Call-by-Value vs Call-by-Name approach
overlays
without overlay

Lecture 4: Recovering confluence: by polarisation and focusing
overlays
without overlay

Lecture 5: Introduction to classical realisability

Exercise sheet