Preuves Interactives et Applications
2016–17
Master Informatique parcours FIIL

Burkhart Wolff (wolff@lri.fr) et Christine Paulin-Mohring (paulin@lri.fr)

http://www.lri.fr/~paulin/PreuvesInteractives

Nouvelles

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

2  Organisation

Evaluation

Planning

3  Plan

  1. (C. Paulin) Introduction, motivations, lambda-calcul simplement typé.
  2. (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.
  3. (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.
  4. (C. Paulin) Exemple de modélisation en Coq.
  5. (B. Wolff) Exemple de modélisation en Isabelle/HOL.
  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)

4  Projet

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