Validationprojet
EnseignantAlexis Saurin
Horaires hebdomadaires 2.0 h CM , 2.0 h TP
Années Master Logique Mathématique et Fondements de l'Informatique M2 Logos

Syllabus

Une moitié des heures de ces modules consistera en des cours, l’autre en des TP sur machine. Ces cours se concluront par un projet à réaliser en Coq. Le contenu de ces cours est un prérequis pour le cours de théorie des types homotopiques.

Sommaire

Programmation fonctionnelle en Coq

  • Lambda-calcul, récursivité (et ses limites en Coq), typage à la ML
  • Structures de données usuelles (booléens, entiers, listes, options, arbres, ...)
  • Programmation générique : polymorphisme, modules, classes de type
  • Types dépendants
  • Lien avec d'autres langages comme OCaml, présentation des "absents" de Coq (exceptions, traits impératifs, entrées-sorties, ...), comment faire le lien entre OCaml et Coq

Preuves formelles en Coq

  • Langage de spécification, règles logiques de base
  • Arithmétique, calcul, réécriture, récurrence
  • Preuves de propriétés des structures de données usuelles
  • Prédicats inductifs
  • Automatisation
  • Éventuellement: rapide tour d'horizon d'autres assistants de preuves et comparaison avec Coq

Bibliographie