3/01/2023: Lecture 1 by Thomas C.
6/01/2023: Lecture 1 – Proof-program correspondence for Peano's arithmetic (first-order), System T and its normalization theorem, structure of the strong normalization proof by reducibility.
10/01/2023: Lecture 2 by Thomas C.
13/01/2023: Lecture 2 – Proving strong normalization for System T.
17/01/2023: Lecture 3 – Introduction to second-order logic, second-order arithmetic, System F and its normalization properties. (planned)
20/01/2023: Lecture 4 – Reducibility candidates and weak normalisation of System F.
24/01/2023: Lecture 3 by Thomas C.
27/01/2023: Lecture 4 by Thomas C.
31/01/2023: Cancelled.
3/02/2023: Lecture 5 – Realizability in System F.
7/02/2023: Lecture 5 by Thomas C.
10/02/2023: Lecture 6 by Thomas C.
14/02/2023: Lecture 7 by Thomas C.
17/02/2023: Lecture by Thomas C is cancelled
21/02/2023: Lecture 6 – Applications of realizability.
24/02/2023: Lecture 7 – Expressiveness of System F.
28/02/2023: no lecture: where were you?
3/03/2023: Lecture 8 by Thomas C.
7/03/2023: Cancelled due to strike
8/03/2023: Lectures 8 et 9 – Representation theorem of System F.
10/03/2023: Mid-term exam
14/03/2023: Lecture 9 by Thomas C.
17/03/2023: Lecture 10 by Thomas C.
21/03/2023: ???
24/03/2023: ???
28/03/2023: ???
31/03/2023: ???