Preuves Interactives et Applications
2015–16
Master Informatique parcours FIIL

Nouvelles

• Premier cours lundi 14 septembre 2015 14h-17h15

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 x) + Examen final (coeff y)
  (seule une feuille A4 manuscripte recto-verso sera autorisée)

Planning

• Cours+TD/TP salle E203 : lundi 14h-15h30 et 15h45-17h15

3  Plan

1. (C. Paulin) Introduction, motivations, lambda-calcul simplement typé.
   • Transparents du cours
   • Squelette Isabelle Squelette Coq
   • Fichiers de démonstration du cours Isabelle, Coq
   • Solution des exercices
     • Modélisation β-réduction : Solution Isabelle, Solution Coq
     • Exercices sur le λ-calcul : Solution Fichier Isabelle
     • Modélisation droits d’accès Solution Isabelle, Solution Coq
2. (B. Wolff) Logique d’ordre supérieur, représentation des termes et des formules en Coq et Isabelle/HOL, preuves élémentaires.
   • Transparents du cours
   • TP Squelette Isabelle Squelette Coq
   • Tutorial Isabelle, Tutorial Coq
3. (C. Paulin) Définitions inductives de types de données et de relation, définitions récursives et preuves par récurrence, représentation en Coq et Isabelle/HOL.
4. (B. Wolff) Exemple de modélisation en Isabelle/HOL.
5. (C. Paulin) Exemple de modélisation en Coq.
6. (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.
7. (C. Paulin& B. Wolff) Applications avancées.

4  Liens utiles

• Assistant de preuves Isabelle-HOL
• Assistant de preuves Coq

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 L^AT_EX par H^EV^EA