Preuves assistées par ordinateur

Preuves assistées par ordinateur
Cursus master ingénierie (CMI)Parcours Cursus master ingénierie (CMI) - Informatique, image, réalité virtuelle, interactions et jeux

ComposanteUFR de mathématique et d'informatique

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.

Disciplines

  • 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

Contacts

Responsable(s) de l'enseignement