===== M2 LMFI: Quantification du second-ordre et points-fixes en logique =====
===== M2 LMFI: Second-order quantification and fixed points in logic (SOFIX) =====

The 2023-2024 SOFIX course is jointly taught by Thomas Colcombet and Alexis Saurin.
See the [[https://master.math.univ-paris-diderot.fr/modules/m2lmfi-second-ordre/|description of the course]] on the LMFI website

/* 
=== Presentation of research papers ===

[[https://www.irif.fr/users/saurin/teaching/lmfi/sofix-2022/paper-presentation|Page listing papers for the presentation]]
*/

=== Partie sur la théorie de la preuve du second-ordre et du mu-calcul ===
=== Part on the proof theory of second-order logic and of the mu-calculus ===


== Planning and Lecture notes / Notes de cours: ==

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

  * 10/01/2024: **<color #00a2e8>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).</color>** 
    * 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
    * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/cours-01-t.pdf|Lecture notes on system T]].
  * 12/01/2024: **<color #00a2e8>Lecture 2 -- Complements on system F; Introduction to second-order logic, second-order natural deduction and second-order arithmetic.</color>** 
    * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/cours-02-so-pa2.pdf|Lecture notes on second-orer logic and PA2]].
  * 17/01/2024: **<color #00a2e8>Lecture 3 -- Normalization theorems for System F.</color>** 
    * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/cours-03-f-wn.pdf|lecture notes introducing System F and proving weak-normalization by reducilibility candidates]].
/* [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix3.pdf|Introduction to System F and its normalization properties]] (version of the 13/01/22) (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-3.pdf|whiteboard]])*/
  * <color #c3c3c3>19/01/2024: Lecture 1 by Thomas C.</color>
  * <color #c3c3c3>24/01/2024: Lecture 2 by Thomas C.</color> 
  * <color #c3c3c3>26/01/2024: Lecture 3 by Thomas C.</color> 
  * <color #c3c3c3>31/01/2024: Lecture 4 by Thomas C.</color> 
  * <color #c3c3c3>2/02/2024: Lecture 5 by Thomas C.</color> 
  * 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: **<color #00a2e8>Lecture 4 -- Expressive power of Second-order logic. (material to come)</color>** 
  * 14/02/2024: **<color #00a2e8>Lecture 5 -- Expressive power of System F.</color>** 
    * 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) [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/slides-provably-total-functions.pdf|slides on probably total functions]]
    * 2) [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/slides-f-expressiveness.pdf|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.)
  * <color #c3c3c3>16/02/2024: No Lecture.</color>
  * <color #c3c3c3>21/02/2024: Lecture 6 by Thomas C.</color>
  * <color #c3c3c3>23/02/2024: Lecture 7 by Thomas C.</color>
  * <color #c3c3c3>28/02/2024: Lecture 8 by Thomas C.</color> 
  * <color #c3c3c3>1/03/2024: Lecture 9 by Thomas C.</color> (postponed to leave the slot free for Logic in Paris)
  * <color #c3c3c3>6/03/2024: Lecture 9 by Thomas C.</color> 
  * <color #c3c3c3>8/03/2024: Lecture 10 by Thomas C.</color> 
  * 13/03/2024: **<color #00a2e8>Lecture 6 -- Planning to start the study of proof theory of mu-calculus.</color>** 
/*    * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-06.pdf|lecture notes corresponding to the sixth lecture, SN of F and other application of realizability.]]
*/
  * 15/03/2024: **<color #00a2e8>Lecture 7 -- .</color>** 
  * <color #c3c3c3>20/03/2024: Lecture 11 by Thomas C.</color>
  * 22/03/2024:   **<color #00a2e8>Lectures 8 ([[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/lmfi.pdf|slides]]).</color>**
  * <color #c3c3c3>27/03/2024: Lecture 12 by Thomas C.</color>
  * <color #c3c3c3>29/03/2024: Lecture 13 by Thomas Colcombet.</color>
  * 3/04/2024: **<color #00a2e8>Lecture 9 ([[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/lmfi.pdf|slides]]).</color>** 
  * 5/04/2024: **<color #00a2e8>Lecture 10.</color>** 
/*  * **<color #00a2e8>Lecture 8 -- Representation theorem of system F</color>** (planned). 
  * **<color #00a2e8>Lecture 9 -- Representation of free structures in system F.</color>** (planned) 
/* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-9.pdf|whiteboard]])*/
  * **<color #00a2e8>Lecture 10 -- Proof theory of the mu-calculus.</color>** (planned) 
/* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-10.pdf|whiteboard]])*/
  * **<color #00a2e8>Lecture 11 -- Proof systems for the (modal) mu-calculus: 2- Infinitary Proof systems for the mu-calculus</color>** (planned) 
/*  (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-11.pdf|whiteboard]])*/
  * **<color #00a2e8>Lecture 12 -- Proof systems for the (modal) mu-calculus: 3- Infinitary proofs with the Omega-rule, relations with other proof systems.</color>** (planned) 
/* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-12.pdf|whiteboard]])*/
*/

== Graded Homework / DM noté: ==

  * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2024/sofix-dm24-part1.pdf|Part I (System F and Proofs in Second-order logic)]]
  * Part II (to come)
/*
   * For friday 13/01: redo the synthesis of System T recursor from the analysis of Peano Induction axioms seen in class and the proof simplification rules I gave you in class. 
   * For friday 20/01: do the exercizes in the notes for lecture 2. 
   * More to come! 
*/

== Bibliographic references / Références bibliographiques: ==

   * //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

/*
== Some old lecture notes, to be updated: ==

   * Basic proof theory and lambda-calculus (corresponding to first semester course):
     *  [[https://www.irif.fr/users/saurin/teaching/lmfi/cf-thdem-2021|Part of the first semester course on proof-theory dedicated to natural deduction and the lambda-calculus]]
   * Some notes on second-order logic and System F
     * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix1.pdf|Gödel's system T (normalization and expressive power)]] (version of the 7/01/22)
     * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix2.pdf|Introduction to second-order logic and arithmetics]] (version of the 7/01/22)
     * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix3.pdf|Introduction to System F and its normalization properties]] (version of the 13/01/22)

*/