The 2023-2024 SOFIX course is jointly taught by Thomas Colcombet and Alexis Saurin. See the description of the course on the LMFI website

(The end of the semester will certainly be adapted wrt this schedule.)

• 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
  • Lecture notes on system T.
• 12/01/2024: Lecture 2 – Complements on system F; Introduction to second-order logic, second-order natural deduction and second-order arithmetic.
  • Lecture notes on second-orer logic and PA2.
• 17/01/2024: Lecture 3 – Normalization theorems for System F.
  • lecture notes introducing System F and proving weak-normalization by reducilibility candidates.
• 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.
  • 1) slides on probably total functions
  • 2) slides on the representation theorem for system F
  • (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.

• Part I (System F and Proofs in Second-order logic)
• Part II (to come)

• Domains and Lambda-calculi, R. Amadio & P-L. Curien
• Rudiments of mu-calculus, A. Arnold & D. Niwinski
• Proofs and Types, J-Y. Girard, P. Taylor & Y. Lafont
• Proof-theory and Logical Complexity, J-Y. Girard
• Practical Foundations for Programming Languages, R. Harper
• Lambda-calculus and Models, J-L. Krivine
• Lectures on the Curry-Howard Isomorphism, M. H. Sørensen & P. Urzyczyn
• Proof Theory, G. Takeuti