Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Assistants de preuves (24h, 3 ECTS)

Responsable : Bruno Barras

Informations pratiques pour 2019-2020

  • Le cours a lieu en salle 1014, le vendredi de 16h15 à 19h15. Attention! Pas de cours le 11 octobre.
  • Il est nécessaire d'apporter un ordinateur portable sur lequel Coq est installé pour les travaux pratiques (version 8.5 ou plus de préférence).
  • Il est demandé un niveau de pratique de Coq minimal. Pour cela, il est conseillé de suivre *une* des méthodes introductives citées plus bas (ou bien le début pour les plus elaborées).

Intervenants pour 2019-2020

Objectifs

L’objectif prinicipal de ce cours est de développer la maîtrise de l’assistant à la preuve Coq, ainsi que les connaissances théoriques indispensables à la bonne compréhension et au bon emploi du formalisme implanté. Cette partie théorique donnera un apperçu de la problématique de la recherche en Théorie des Types.

Le point essentiel, qui fait la particularité de Coq, est la notion générale de type inductif, qui est un ingrédient quasiment indispensable dans la plupart des modélisations, que ce soit dans le cas de structures algébriques abstraites ou de structures de données concrètes.

Plan du cours

Le corps principal de ce cours est formé de 5 séances de 3h abordant les sujets suivants:

  1. Rappels et mise à niveau (2 séances): lambda-calcul, types dépendents, isomorphisme de Curry-Howard, Calcul des Constructions.
  2. Introduction au Calcul des Constructions Inductives et au système Coq. Du calcul des constructions pur aux constructions inductives.
  3. Les spécificités du Calcul des Constructions Inductives : égalité de Leibniz, arbres à branchement infini, inductifs mutuels, inductifs imbriqués. Théorie des définitions inductives: contrainte de positivité stricte, restrictions d'élimination, types singletons, définition par point-fixe.
  4. Modélisation de structures mathematiques, de structures de données, constructions monadiques. Utilisation de structures canoniques et de typeclasses. Liens entre une structure abstraite et ses représentations.

Le module se terminera avec 3 séances qui traiteront de points pris dans la liste suivante:

  1. Réalisabilité, extraction de programmes à partir de preuves.
  2. Programmation fonctionnelle : récursion structurelle versus accessibilité, fonctions partielles, définitions co-inductives.
  3. Calcul efficace: réflexion calculatoire, certification d'algorithmes efficaces.
  4. Modèles du Calcul des Constructions. Résultats d'indépendance.
  5. Programmation par types dépendants, filtrage dépendant.
  6. Théorie des types homotopique.

Chaque séance se composera d'une moitié enseignement magistral et d'une moitié de travaux pratiques sur machine.

Evaluation du module

  • Examen écrit, durée 3h.
  • 1 Exercice en Coq à préparer individuellement, à partir de la moitié du cours. Cet exercice consistera à implanter des définitions ou prouver des lemmes (remettre le fichier source), et expliquer les choix de modélisation ou difficultés rencontrées (document PDF).

Langues du cours

Français de préférence mais le cours pourra être fait en anglais suivant demande.

Supports de cours

Polycopié “Assistants de Preuves” (PDF, HTML). Attention, ce polycopié est lié à une version antérieure du cours : il ne couvre ainsi pas la totalité de ce qui sera abordé mais traite aussi de sujets qui ne sont pas au programme de cette année.

Transparents cours et TPs

Cette section se remplira cours après cours...

Pré-requis

Programmation
un langage fonctionnel (Ocaml)
Langages
typage (systèmes de types élémentaires, inférence de type à la ML)
Logique
calcul propositionnel, logique du premier ordre, systèmes de preuves en déduction naturelle
Calculabilité
lambda-calcul pur (syntaxe, alpha-conversion, beta-réduction, confluence, normalisation)
Mathématique
ordres bien fondés

Cours liés

Ce cours s'appuie sur le cours de M2 2-7-1: Fondements des systèmes de preuves. Certaines notions du cours 2-5: démonstration automatique peuvent être utiles.

En complément, le cours 2-36-1: Preuves de programmes est particulièrement indiqué.

Stages liés au cours

Bibliographie

Méthodes d'introduction à Coq:

  • Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions.
    Texts in Theoretical Computer Science. An EATCS Series (2004), Springer.
    Une version française est librement disponible ici.
  • B. C. Pierce, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hriţcu, V. Sjöberg, B. Yorgey. Software Foundations.

Autres documents liés au cours:

  • B. Nordström, K. Petersson, J. Smith. Programming in Martin-Löf's Type Theory, Clarendon Press, Oxford (1990).
  • Documentation de l'assistant de preuve Coq.
  • The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory.

Les années précédentes

Équipe pédagogique

  • Bruno Barras, Chargé de Recherche INRIA Saclay - Île-de-France
  • Matthieu Sozeau, Chargé de Recherche INRIA Paris
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA