===== M2 LMFI: Quantification du second-ordre et points-fixes en logique ===== ===== M2 LMFI: Second-order quantification and fixed points in logic (SOFIX) ===== === 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 === == Lecture notes / Notes de cours: == * 4/01/2022: Lecture 1 -- [[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) (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-1.pdf|whiteboard]]) * 7/01/2022: Lecture 2 -- [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix2.pdf|Introduction to second-order logic and arithmetics]] (version of the 7/01/22) (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-2.pdf|whiteboard]]) * 11/01/2022: Lecture 3 -- [[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]]) * 14/01/2022: Lecture 4 -- Realisability in System F and strong normalization theorem (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-4.pdf|whiteboard]], until slide 11) * 18/01/2022: Lecture by Thomas C * 21/01/2022: Lecture by Thomas C * 25/01/2022: Lecture by Thomas C * 28/01/2022: Lecture by Thomas C * 1/02/2022: Lecture by Thomas C * 4/02/2022: Lecture 5 -- End of lecture on strong normalization of system F (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-5.pdf|whiteboard]]) * 8/02/2022: Lecture 6 -- Expressiveness of second-order logic, Knaster-Tarski fixed-point theorem, Defect of the standard semantics (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-6.pdf|whiteboard]]) * 11/02/2022: Lecture 7 -- Full models and Henkin models of second-order logic, completeness of second-order logic wrt Henkin's models (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-7.pdf|whiteboard]]) * 15/02/2022: Lecture 8 -- Representation theorem of system F (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-8.pdf|whiteboard]]) * 18/02/2022: Lecture by Thomas C * 22/02/2022: Lecture by Thomas C * 25/02/2022: Lecture by Thomas C * 1/03/2022: Lecture 9 -- Representation of free structures in system F (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-9.pdf|whiteboard]]) * 4/03/2022: cancelled * 8/03/2022: Lecture by Thomas C * 11/03/2022: Lecture by Thomas C * 15/03/2022: Lecture 10 -- Proof theory of the mu-calculus (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-10.pdf|whiteboard]]) * 18/03/2022: Lecture 11 -- Proof systems for the (modal) mu-calculus: 2- Infinintary Proof systems for the mu-calculus (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-11.pdf|whiteboard]]) * 22/03/2022: Lecture 12 -- Proof systems for the (modal) mu-calculus: 3- Infinitary proofs with the Omega-rule, relations with other proof systems) (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-12.pdf|whiteboard]]) * 25/03/2022: Lecture by Thomas C == 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 == Additional content / Contenu supplémentaire: == [[https://www.irif.fr/users/saurin/teaching/lmfi/cf-thdem-2021|Part of the first semester cours on proof-theory dedicated to natural deduction and the lambda-calculus]]