Archive 2019
Validationexamen
EnseignantThierry Joly
Horaires hebdomadaires 2 h CM , 2 h TD
Années Master Logique et Fondements de l'Informatique

Syllabus

  • Théorème de complétude du calcul des séquents égalitaire LK par les témoins de Henkin.
  • Calcul des séquents : Élimination des coupures et théorème du séquent médian dans LK. Théorème de Herbrand. Sous-calcul LJ : la logique intuitionniste et son interprétation BHK. Propriétés de la sous-formule et du témoin existentiel dans LJ.
  • Déduction naturelle : Systèmes NK et NJ. Élimination des coupures de NJ. Propriétés de la sous-formule et du témoin existentiel dans NJ, puis dans HA (arithmétique intuitionniste).
  • Lambda-calcul : Propriétés de confluence et de standardisation. Représentation des fonctions récursives. Système T. Correspondance de Curry-Howard. Réalisabilité, normalisation forte et correction des programmes.

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, 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).