Program requirementsexamen
TeacherAlexis Saurin, , Dominik Kirst
Weekly hours 2 h CM , 2 h TD
Years Master Logique Mathématique et Fondements de l'Informatique M2 Logos

Syllabus

  • Sequent calculus: Study of LK and LJ sequent calculi. Completeness theorem for LK. Cut elimination theorem and its applications (for LK: mid-sequent theorem, Herbrand's theorem, Craig-Lyndon interpolation; for LJ: disjunction property and existential witness property).
  • Natural deduction: NK and NJ systems. BHK interpretation, Cut elimination in NJ. HA (Heyting Arithmetic).
  • Intuitionistic logic: BHK interpretation, Kripke models, double negation translations.
  • Pure lambda-calculus: Confluence and standardization theorems. Representation of recursive functions. Separation theorem and Böhm trees.
  • Simply typed lambda-calculus and System T: Curry-Howard correspondence. strong normalisation and program correctness.
  • Opening topics: depending on time remaining, we will outline some additional topics (system F, dependent type theory, Curry-Howard for classical logic and term calculi for sequent proofs, linear and modal logic)

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, 2nd ed. 2019).
- J.-Y. GIRARD: Proof Theory and Logical Complexity (Bibliopolis, 1987).
- 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-calculus : Types and Models (Ellis Howood, 1993, available on the author's webpage).
- M.H. SORENSEN, P. URZYCZYN. Lectures on the Curry-Howard Isomorphism (Elsevier, 2006).
- A.S. TROELSTRA & D. VAN DALEN. Constructivism in mathematics, Vol. I (North-Holland, 1988).
- A.S. TROELSTRA & H. SCHWICHTENBERG: Basic Proof Theory (Cambridge University Press, 2000).