 BBB classroom.
 Lecturers:
 Tutorials by Étienne Miquey.
Overview
The objective of this course is to provide the basics of the theory underlying the Coq proof assistant,
namely the CurryHoward correspondence between proofs and programs.
Technically, we will investigate intuitionistic logics and their relations to typed λcalculi.
Prerequisites:

We assume some familiarity with computability theory and mathematical logic,
essentially
corresponding to the courses Fondements de l'informatique and Logique given in the
L3 year of the Computer Science Department of ENS de Lyon.
Bibliography:

The course is loosely based on the reference book:

Sørensen, M. H. et Urzyczyn, P.,
Lectures on the CurryHoward Isomorphism,
volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006.

Sørensen, M. H. et Urzyczyn, P.,
Lectures on the CurryHoward Isomorphism,
Homeworks

Confluence of the (Pure) Untyped λCalculus
 The homework in [pdf].
 To be completed for the 23rd of Feb. 2021 (see instructions inside).

Friedman's Translation
 The homework in [pdf].
 To be completed for the 15th of March 2021 (see instructions inside).
Courses

Course 1 (Jan. 19th)
[slides]
[scan]
 Introduction to the course.
 Natural Deduction for Intuitionistic Propositional Logic.

Course 2 (Jan. 26th)
 Negative Translation for Propositional Logic [slides] [scan].
 The (Pure) Untyped λCalculus [notes on αequivalence] [scan].

Course 3 (Feb. 2nd)
[slides]

Course 5 (Feb. 23rd)
[slides]
 Natural Deduction for Predicate (i.e. FirstOrder) Logic [scan].
 FirstOrder Arithmetic [definition of PA* and HA*] [scan].
 Gödel's System T, the Representation Theorem and Modified Realizability [scan].

Course 6 (Mar. 2nd)
[slides]
 Comments on the Homework (Confluence) [scan].
 SecondOrder Logic [notes on Henkin models] [scan].
 ChurchStyle System F (a.k.a. Polymorphic λCalculus) [scan].

Course 7 (Mar. 9th)
[scan]
 CurryStyle System F [slides].

Strong Normalization of System F
(see also the [notes on normalization] (for simple types)).

Course 8 (Mar. 16th)

Course 10 (Mar. 30th)
 Examples in SecondOrder Logic [preliminary notes].
Back home.