Programmation fonctionnelle et preuve formelle en COQ
Code APOGÉE : MA2DE080 | 6 ECTS | Enseignant : Alexis Saurin | Validation : projet
Horaires hebdomadaires : 2h CM, 2h TP | Mutualisé avec : M2 LMFI
Une moitié des heures de ce module consistera en des cours, l’autre en des TP sur machine. Ce cours se conclura par un projet à réaliser en Coq. Le contenu de ce cours est un prérequis pour le cours de théorie des types homotopiques.
Programme
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
Modalités d’évaluation
Évaluation par projet à réaliser en Coq.
Bibliographie
- David, R., Nour, K. & Raffalli, C. (2001). Introduction à la logique : théorie de la démonstration. Paris : Dunod.
- Bertot, Y. & Castéran, P. (2004). Interactive Theorem Proving and Program Development. Coq’Art : The Calculus of Inductive Constructions. Berlin : Springer Verlag. Disponible en ligne : http://www.labri.fr/perso/casteran/CoqArt
- Wiedijk, F. (Ed.) (2006). The Seventeen Provers of the World. LNCS vol. 3600. Berlin : Springer Verlag. Disponible en ligne : http://www.cs.ru.nl/~freek/comparison/comparison.pdf