Archive 2020
Program requirementsexamen
TeacherAlexis Saurin
Weekly hours 2 h CM , 2 h TD
Years Master Logique et Fondements de l'Informatique

Syllabus

  • Completeness theorem of the LK sequent calculus with equality by Henkin's witnesses.
  • Sequent calculus: cut elimination of and median sequent theorem in LK. Herbrand's theorem. LJ sub-calculation: intuitionist logic and its BHK interpretation. Properties of the sub-formula and existential witnesses in LJ.
  • Natural deduction: NK and NJ systems. Cut elimination in NJ. Properties of the sub-formula and existential witnesses in NJ, then in HA (intuitionist arithmetic).
  • Lambda-calculus: Confluence and standardization properties. Representation of recursive functions. T system. Curry-Howard correspondence. Realizability, strong standardization and program correctness.

Bibliography

  • R. CORI, D. LASCAR. Logique mathématique, tomes 1 & 2 (Dunod, 2003).
  • R. DAVID, K. NOUR, C. RAFFALLI. Introduction à la logique - Théorie de la démonstration (Dunod, 2004).
  • A.S. TROELSTRA & D. VAN DALEN. Constructivism in mathematics, Vol. I (North-Holland, 1988).
  • J.-Y. GIRARD, Y. LAFONT & P. TAYLOR : Proofs and Types (Cambridge University Press, 1989, disponible sur la page de P. Taylor).
  • J.-L. KRIVINE. Lambda-calcul : Types et Modèles (Masson, 1990, existe en version anglaise et augmentée, disponible sur la page de l'auteur).