Module PP : Preuves et programmes, une introduction à l'aide du système Coq

Module PP : Preuves et programmes, une introduction à l'aide du système Coq

Equipe pédagogique :

Catherine Parent-Vigouroux, François Puitg

Volume :

12h.

Spécialité :

S&L

N.B. Ce module est commun aux parcours FTI et VSC.

L'Informatique est un élément central dans de plus en plus de systèmes critiques où l'erreur n'est pas tolérable (avionique, métro automatique etc.). Dans la quête de systèmes "parfaits", les méthodes formelles suscitent aujourd'hui un enthousiasme croissant, non seulement dans les laboratoires de recherche, mais aussi dans le monde industriel.

Une spécification formelle est un point de vue abstrait indépendant de toute implantation décrivant de manière rigoureuse les composants et le comportement d'un système. Ainsi des propriétés telles que la validité d'une axiomatisation, l'équivalence de deux concepts ou la terminaison d'un programme peuvent être démontrées.

Ce cours est une introduction aux spécifications formelles et à la preuve de programmes à partir d'un formalisme qui est le Calcul des Constructions et l'outil Coq associé, notamment dans le but d'extraire des programmes certifiés.

Connaissances / Méthodes acquises :

• Fondement de la théorie de la preuve.
• Démonstration par induction structurelle (termes et types).
• Utilisation d'un assistant de preuve

Plan du cours

1. Notions de théorie des types -- Les langages logiques d'ordre 1 : terme, proposition, connecteurs -- Les langages logiques d'ordre supérieur : fonction, abstraction, application,beta-réduction -- Lambda-calcul typé : typage des lambda-termes -- Théorie des types : typage des propositions
2. Isomorphisme de Curry-Howard, déduction naturelle et sémantique de Brouwer-Heyting-Kolmogorov
3. Induction et récursion -- Objets inductifs -- Types inductifs non récursifs, analyse par cas -- Types inductifs récursifs, induction
4. Extraction de programmes certifiés

Module PP : Preuves et programmes, une introduction à l'aide du système Coq