WikiMPRI

Responsable : Gilles Dowek

1. ??? (14h, Gilles Dowek
2. ??? (10h, Alexandre Miquel

(essentiellement TD)

Responsable : Chritine Paulin

1. ??? (12h, Bruno Barras
2. ??? (12h, Jean-Christophe Filliatre

Ce cours étudie la notion de preuve en tant qu'objet mathématique et informatique. Il présente plusieurs théories logiques en mettant l'accent sur les théories des types d'ordre supérieur. Il s'intéresse plus particulièrement à l'articulation entre les notions de raisonnement et de calcul. Les concepts présentés servent de base à plusieurs assistants de preuves, en particulier le système Coq; ils ont pour application la vérification de programmes et la mécanisation de théories mathématiques.

1. Logique du premier ordre : système de Hilbert, déduction naturelle, calcul des séquents. Propriétés : élimination des coupures, traductions. Extension au cas multisortes.
2. Déduction modulo.
3. La théorie des ensembles, la théorie des types simples.
4. Lambda-calcul simplement typé : normalisation.
5. Expression et existence de fonctions en théorie des types : fonctions exprimables sur les entiers de Peano, les entiers de Church; opérateur de choix et de description; représentation de fonctions en logiques intuitionniste ou classique.
6. Logique intuitionniste, isomorphisme de Curry-de Bruijn-Howard, types dépendants.
7. Types inductifs : système T de Gödel et théorie des types de Martin-Löf.
8. Polymorphisme : système F, Calcul des Constructions, généralisation aux systèmes de types purs. Normalisation, élimination des coupures, représentation des fonctions.
9. Introduction au système Coq.
10. Définitions de relations inductives et co-inductives : paradoxes, applications à la modélisation de la sémantique des langages de programmation.
11. Calcul des Constructions Algébriques.
12. Réalisabilité, extraction de programmes à partir de preuves constructives.
13. Programmation avec types dépendants, lien avec la preuve de programmes.
14. Architecture des assistants de preuves : Coq, PVS, Isabelle.
15. Preuves constructives en logique classique, relation avec les programmes et les machines de réduction.

Programmation

un langage fonctionnel (Ocaml)

Langages

typage (systèmes de types élémentaires, inférence de type à la ML)

Logique

calcul propositionnel, logique du premier ordre, systèmes de preuves en déduction naturelle

Calculabilité

lambda-calcul pur (syntaxe, alpha-conversion, béta-réduction, confluence)

Mathématique

ordres bien fondés

Réécriture

Notions de base de réécriture du premier ordre

• B. Nordström, K. Petersson, J. Smith. Programming in Martin-Löf's Type Theory.
• The Coq Proof Assistant V7 [[http://coq.inria.fr/doc-fra.html|http://coq.inria.fr/doc-fra.html]].
• G. Dowek. Théorie des Types.