Description

Les assistants à la preuve sont des logiciels qui permettent de construire et de manipuler des preuves formelles. On les utilise pour vérifier des résultats mathématiques et pour certifier des programmes.

Cette UE propose une introduction aux méthodes formelles en mathématiques et en informatique, on apprendra en particulier à utiliser le logiciel Rocq pour écrire des preuves formelles.

Compétences requises

À l'entrée de cet enseignement, un(e) étudiant(e) devrait :

- Savoir exprimer un énoncé dans le calcul propositionnel et/ou calcul  des prédicats.

- Être familiers avec la programmation en style fonctionnel, en  particulier les fonctions récursives et types de données les plus  communs (listes, arbres, etc.)

- Savoir rédiger correctement une preuve par récurrence sur les entiers.

Compétences visées

À l'issue de cet enseignement, un(e) étudiant(e) saura :

- Prouver des propositions mathématiques à l’aide d’un assistant  à la preuve comme Rocq ou Lean.

- Savoir faire des preuves par récurrence structurelle sur des  structures plus complexes que les entiers.

- Spécifier et implanter des structures de données et des opérations  sur ces structures, prouver des propriétés de ces objets.

- Avoir des notions de théorie des types.

Disciplines

• Informatique

Syllabus

- Motivations. Utilisations des assistants à la preuve en mathématiques et en informatique. Tour d'horizon des différents assistants à la preuve.

- Arbres de dérivation.

- Preuves en logique propositionnelle et calcul des prédicats.

- Langages d’interaction à base de tactiques.

- Types énumérés, types produit et types somme.

- Structures de données inductives (entiers naturels, listes, arbres), prédicats inductifs.

- Fonctions récursives structurelles, preuves par récurrence.

- Types enregistrements, structures algébriques.

- Polymorphisme et arguments implicites.

- Logique intuitionniste, logique classique. Théorie des types. Correspondance de Curry-Howard.

Bibliographie

• Yves Bertot, 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. 2004
• Adam Chlipala. Certified Programming with Dependent Types. MIT Press. 2013. ISBN: 9780262026659
• Benjamin Pierce et al. Software Foundations. Volume 1: Logical Foundations. 2007
• Benjamin Pierce et al. Software Foundations. Volume 3: Verified Functional Algorithms. 2007

Contacts

Responsable(s) de l'enseignement

• Loïc Pujet