The Coq mailing list

[Steve Kremer <kremer AT lsv.ens-cachan.fr>]

                               Séminaire
                 Laboratoire Spécification et Vérification
                        http://www.lsv.ens-cachan.fr/




Mardi 23 novembre 2004, à 11 h, Salle Condorcet (bâtiment d'Alembert)


Pierre Letouzey (Ludwig-Maximilians-Universitat Munchen) fera un exposé sur

"Extraction en Coq et preuves de programmes modulaires"

Abstract:


L'assistant de preuves Coq comporte de longue date un mécanisme nommé 
extraction. Cet outil permet d'engendrer automatiquement des programmes 
certifiés corrects à partir de preuves constructives formalisées en Coq. 
Ces programmes extraits sont exprimés dans des langages fonctionnels, à 
savoir Ocaml ou Haskell.

Dans le cadre de ma thèse récemment terminée, cette extraction Coq a 
subie une refonte complète, afin d'étendre son champs d'application. 
L'outil précédent présentait en effet d'importantes limitations, 
refusant certaines preuves Coq, et conduisant même parfois à des 
programmes extraits incorrects. Dans un premier temps, je présenterai un 
rapide état des lieux de la nouvelle extraction Coq à l'issue de ma 
thèse, tant au niveau de l'implantation que des garanties théoriques de 
correction.

Je mettrai ensuite l'accent sur une nouvelle caractéristique 
particulièrement séduisante dans l'optique de preuves de programmes 
réalistes, à savoir la possibilité de certifier puis d'extraire des 
programmes modulaires. En effet, Coq comporte désormais un système de 
modules, signatures et foncteurs similaire à celui d'Ocaml, et la 
nouvelle extraction permet de faire un pont entre les deux systèmes. Je 
présenterai en particulier la certification de la bibliothèque standard 
d'ensembles finis d'Ocaml réalisée en collaboration avec J.C. Filliâtre.

Cordialement,

---
Steve Kremer

Laboratoire Spécification et Vérification
CNRS UMR 8643 & INRIA Futurs projet SECSI & École Normale Supérieure de 
Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex - France
kremer AT lsv.ens-cachan.fr
                http://www.lsv.ens-cachan.fr/~kremer
Tel.: ++ 33 1 47 40 75 45               Secret.: ++ 33 1 47 40 75 20
Fax : ++ 33 1 47 40 75 21               Office : RH-B-102