Théorie de la démonstration

Cours de recherche (30h de cours, travail sur des articles scientifiques)

Cours : Alexandre Miquel, Olivier Laurent (Alexandre.Miquel,Olivier.Laurent)

La correspondance de Curry-Howard (qui relie les objets et les concepts de la logique à ceux de la programmation) a considérablement renouvelé les outils et méthodes de la théorie de la démonstration grâce au nouvel éclairage porté sur la dynamique calculatoire des preuves. Ce cours se propose de montrer comment les idées de base de cette correspondance (formule = type, preuve = programme, élimination des coupures = calcul) peuvent se décliner techniquement de manières assez diverses, que ce soit à travers les systèmes de types utilisés par les assistants à la démonstration (Coq) ou à travers les modèles de réalisabilité qui sont à la base des mécanismes d’extraction de programme à partir de preuves classiques. On abordera notamment les points suivants:

• Systèmes de types pour le calcul des prédicats intuitionniste et l’arithmétique de Heyting
• Le système F à la Church et à la Curry, équivalence avec l’arithmétique (intuitionniste et classique) du second ordre
• Types dépendants: systèmes de types purs (PTS), calcul des constructions et types inductifs
• Extension de la correspondance de Curry Howard à la logique classique, systèmes de types et lambda-calculs classiques
• Bases de la réalisabilité intuitionniste (Kleene) et classique (Krivine), liens avec le typage
• Modèles de réalisabilité classique et extraction de programme à partir de preuves classiques, propriété du témoin en logique classique
• Extensions de la réalisabilité à l’axiome du choix et à la théorie des ensembles, liens et différences avec le forcing

Bibliographie

• G. Dowek. Théorie des types. Cours de M2.
• J.-Y. Girard, Y. Lafont, P. Taylor. Proofs and Types. Cambridge University Press, 1989.
• J.-L. Krivine. Lambda-calcul, types et modèles. Masson, 1990
• J.-L. Krivine. Realizability in classical logic. Cours d’École doctorale à l’Université de Marseille Luminy (mai 2004, dernière révision juil. 2005). À paraître dans Panoramas et synthèses, Société Mathématique de France. HAL.