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

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 – Gödel's system T (normalization and expressive power) (version of the 7/01/22) (additional material: whiteboard)
  • 7/01/2022: Lecture 2 – Introduction to second-order logic and arithmetics (version of the 7/01/22) (additional material: whiteboard)
  • 11/01/2022: Lecture 3 – Introduction to System F and its normalization properties (version of the 13/01/22) (additional material: whiteboard)
  • 14/01/2022: Lecture 4 – Realisability in System F and strong normalization theorem (additional material: 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: whiteboard)
  • 8/02/2022: Lecture 6 – Expressiveness of second-order logic, Knaster-Tarski fixed-point theorem, Defect of the standard semantics (additional material: 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: whiteboard)
  • 15/02/2022: Lecture 8 – Representation theorem of system F (additional material: 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: 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: whiteboard)
  • 18/03/2022: Lecture 11 – Proof systems for the (modal) mu-calculus: 2- Infinintary Proof systems for the mu-calculus (additional material: 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: 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:

Part of the first semester cours on proof-theory dedicated to natural deduction and the lambda-calculus