Validationexamen
EnseignantAlexis Saurin, Dominik Kirst
Horaires hebdomadaires 2 h CM , 2 h TD
Années Master Logique Mathématique et Fondements de l'Informatique M2 Logos

Syllabus

  • Calcul des séquents : Étude des calculs des séquents classique (LK) et intuitioniste (LJ). Théorème de complétude du calcul des séquents LK. Élimination des coupures et ses applications (pour LK: théorème du séquent médian, théorème de Herbrand, interpolation de Craig-Lyndon; pour LJ: propriétés de la disjonction et du témoin existentiel).
  • Déduction naturelle : Systèmes NK et NJ. Élimination des coupures de NJ. Arithmétique de Heyting (HA).
  • Logique intuitioniste: Interpretation BHK. Modèles de Kripke. Traductions par double négation.
  • Lambda-calcul pur: Confluence et standardisation. Représentation des fonctions récursives. Théorème de séparation et Arbres de Böhm.
  • Lambda-calcul simplement typé et Système T: Correspondance de Curry-Howard. normalisation forte et correction des programmes.
  • Sujets d'ouverture : en fonction du temps disponible en fin de semestre, on abordera quelques sujets d'ouverture (possibilités: système F, théorie des types dépendants, Curry-Howard pour la logique classique, calcul de termes pour les preuves en séquents, logiques linéaire et modale)

Sommaire

Bibliographie

- 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-calcul : Types et Modèles (Masson, 1990, disponible en anglais sur la page de l'auteur).
- 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).