10/01/2024: Lecture 1 – Proof-program correspondence for Peano's arithmetic (first-order), System T and its normalization theorem, structure of the strong normalization proofs by reducibility, introduction to system F (Church and Curry style).
For Friday 12/01: 1) redo the synthesis of System T recursor from the analysis of Peano Induction axiom and the proof simplification rules I gave you in class, 2) try to synthesize your proposal for a second-order logic and second-order natural deduction from the types and terms of Church-style system F
-
12/01/2024: Lecture 2 – Complements on system F; Introduction to second-order logic, second-order natural deduction and second-order arithmetic.
17/01/2024: Lecture 3 – Normalization theorems for System F.
19/01/2024: Lecture 1 by Thomas C.
24/01/2024: Lecture 2 by Thomas C.
26/01/2024: Lecture 3 by Thomas C.
31/01/2024: Lecture 4 by Thomas C.
2/02/2024: Lecture 5 by Thomas C.
7/02/2024: This day, there is an IRIF colloquium by Véronique Cortier, we will move the lecture. (to be decided)
9/02/2024: Lecture 4 – Expressive power of Second-order logic. (material to come)
14/02/2024: Lecture 5 – Expressive power of System F.
The aim of the lecture is to prove the following theorem:
Thm: the arithmetical functions that can be represented in System F are exactly those total recursive functions that are provably total in PA2.
-
-
(I'll try to merge the two sets of slides and to publish soon the corresponding lecture notes.)
16/02/2024: No Lecture.
21/02/2024: Lecture 6 by Thomas C.
23/02/2024: Lecture 7 by Thomas C.
28/02/2024: Lecture 8 by Thomas C.
1/03/2024: Lecture 9 by Thomas C. (postponed to leave the slot free for Logic in Paris)
6/03/2024: Lecture 9 by Thomas C.
8/03/2024: Lecture 10 by Thomas C.
13/03/2024: Lecture 6 – Planning to start the study of proof theory of mu-calculus.
15/03/2024: Lecture 7 – .
20/03/2024: Lecture 11 by Thomas C.
22/03/2024:
Lectures 8 (slides).
27/03/2024: Lecture 12 by Thomas C.
29/03/2024: Lecture 13 by Thomas Colcombet.
3/04/2024:
Lecture 9 (slides).
5/04/2024: Lecture 10.