Preuves assistées par ordinateur

Description

Cet enseignement présente une introduction à la vérification formelle des preuves et les assistants de preuve en utilisant le programme Coq. Cette matière développe des outils pour comprendre l'interaction entre la formalisation des résultats mathématiques et la programmation.

Compétences requises

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

• Savoir exprimer un énoncé dans le calcul propositionnel et/ou calcul des prédicats.
• Connaître les règles de la déduction naturelle et savoir construire une dérivation sous forme d’arbres.
• Avoir une expérience de programmation en style fonctionnel (fonctions récursives, listes, arbres, types algébriques de données, filtrage, fonctions d’ordre supérieur).
• Savoir rédiger correctement une preuve par récurrence sur les entiers.

Compétences visées

À l'issue de cet enseignement un étudiant saura :

• Prouver une proposition mathématique simple à l’aide d’un assistant de preuves.
• Spécifier et implanter des structures de données et des opérations sur ces structures, prouver des propriétés de ces objets.
• Savoir faire des preuves par récurrence structurelle sur des structures autres que les entiers.

Discipline(s)

• Informatique

Syllabus

• Motivations. Logiciels critiques. Outils pour garantir la fiabilité des logiciels. Exemples d’utilisation des assistants de preuve pour prouver des propriétés mathématiques et la correction de systèmes informatiques critiques.
• 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 (listes, arbres), prédicats inductifs.
• Définitions, filtrage, fonctions récursives structurelles.
• Preuves par récurrence.
• Polymorphisme et arguments implicites.
• Fonctions d’ordre supérieur : fold, map.
• Sémantique de Brouwer/Heyting/Kolmogorov. 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

Contact