Preuves Interactives et Applications
2016–17
Master Informatique
parcours FIIL |
Nouvelles
- Premier cours mercredi 14 septembre 2016 13h30-16h45
1 Présentation
Résumé
La preuve interactive de théorèmes est une technologie qui prend une place de plus en plus importante tant en informatique qu’en mathématiques. Elle s’appuie sur des langages logiques d’une grande expressivité et des implantations garantissant le plus haut niveau de confiance. Parmi les applications, on notera la preuve du théorème de Feit-Thompson, un résultat avancé en théorie des groupes finis ou encore la preuve semi-automatisée de seL4, un noyau sécurisé de Linux correspondant à un système logiciel complexe.
Ce cours est une introduction aux concepts fondamentaux des environnements de preuves interactives de théorèmes et sera illustré par l’apprentissage de deux systèmes majeurs : Coq et Isabelle/HOL. Les exemples porteront sur la modélisation et la preuve de certains aspects des systèmes critiques ainsi que sur l’utilisation des outils de preuves interactives pour modéliser et prouver des propriétés de langages ou de systèmes logiques.
Objectifs
-
Apprendre à utiliser un assistant de preuves interactif d’ordre supérieur pour modéliser des problèmes de vérification.
2 Organisation
Evaluation
-
9h de cours et 12h de TP répartis en 7 séances de 3 heures
- Projet (coeff 1) + Examen final (coeff 2)
Tous les documents de cours accessibles sur cette page (transparents, sujets et corrigés de TD) sont autorisés
Planning
-
Cours+TD/TP : mercredi 13h30-15h00 et 15h15-16h45
3 Plan
-
(C. Paulin) Introduction, motivations, lambda-calcul simplement typé.
- (B. Wolff) Logique d’ordre supérieur, déduction naturelle, représentation des termes et des formules en Coq et Isabelle/HOL, preuves élémentaires.
- (C. Paulin) Définitions inductives de types de données et de relations, définitions récursives et preuves par récurrence, représentation en Coq et Isabelle/HOL.
- (C. Paulin) Exemple de modélisation en Coq.
- (B. Wolff) Exemple de modélisation en Isabelle/HOL.
- (B. Wolff) Techniques de démonstration automatique, cas de la rééecriture (système de réécriture, unification, confluence et terminaison), mise en œuvre dans les assistants de preuve.
- (C. Paulin& B. Wolff)
4 Projet
-
Vous avez le choix entre deux sujets :
-
le premier sur la preuve de la procédure DPLL pour décider de la satisfiabilité d’une formule Enoncé
- le second sur les expressions régulières et
les automates
- Chaque projet peut être réalisé en Coq ou en Isabelle.
- Lire attentivement les instructions sur l’énoncé.
- Date limite de retour : lundi 21 novembre.
5 Examens
6 Liens utiles
Références
-
[1]
-
Yves Bertot and Pierre Castéran.
Interactive Theorem Proving and Program Development. Coq’Art:
The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS series. Springer
Verlag, 2004.
- [2]
-
Lawrence C. Paulson.
Isabelle - A Generic Theorem Prover (with a contribution by T.
Nipkow), volume 828 of Lecture Notes in Computer Science.
Springer, 1994.
- [3]
-
Benjamin C. Pierce.
Types and Programming Languages.
MIT Press, 2002.
- [4]
-
The Coq Development Team.
The Coq Proof Assistant.
Inria.
.
- [5]
-
Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow.
The isabelle framework.
In TPHOLs, pages 33–38, 2008.
Ce document a été traduit de LATEX par HEVEA