Programmation fonctionnelle et preuves
Cours de base (30 h de cours, 30h de TD)
Cours : Yves Bertot (Yves.Bertot à sophia.inria.fr)
TD : Jean Duprat (Jean.Duprat)
Présentation
Lorsque l'on utilise la correspondance de Curry-Howard pour établir un
lien entre la logique des propositions et le lambda-calcul simplement typé,
on est limité au calcul propositionnel par les types simples. On peut
étendre le typage pour introduire de nouveaux degrés de liberté dans
la construction de fonctions bien typées, en particulier avec la notion
de types dépendants. Nous étudierons cette notion de fonction à type
dépendant et explorerons les nouvelles possibilités logiques qu'elles
nous offrent.
Nous étudierons ensuite les approches typées de la description de
structures de données, en nous basant principalement sur les types de
données inductifs, qui généralisent les types de données récursifs et
les constructions de filtrage déjà abordés en programmation
fonctionnelle. Nous verrons comment la synthèse des notions issues du
typage dépendant et des types inductifs permettent également de
prendre en compte la programmation logique pure.
Nous explorerons ensuite plusieurs domaines d'applications de ces
études dont l'objectif sera de montrer la possibilité de construire
des programmes démontrés corrects vis-à-vis de spécifications.
L'ensemble de ces études seront étayées par des expériences effectuées
à l'aide du système de démonstration sur ordinateur Coq.
Plan
Ce plan pourra être modifié au fur-et-à-mesure des cours en fonction
des questions des élèves.
-
Lambda-calcul pur avec types dépendants, Présentation imprédicative de la
logique usuelle.
- Les types de données inductifs, démonstrations par récurrence et
calcul récursif.
- Les propositions inductives, programmation logique et spécifications.
- Sortes et extraction de programmes.
- Récursion bien fondée.
- Programmation impérative.
- Démonstration par réflexion.
Bibliographie
-
COQ home page http://coq.pauillac.fr/
- Y. Bertot, P. Castéran: Interactive Theorem Proving and Program
Development, Coq'Art: The Calculus of Inductive Constructions
(Springer, 2004)
- J.L. Kinke: Lambda-calcul, types et modèles (Masson, 1990)
- Girard, Lafont, Taylor: Proofs and Types
(Cambridge University Press, 1989)