TypiCal

Intervenant: A. Charguéraud

Date et lieu: Jeudi 2 avril 2009, 10h00-12h00, salle de réunion du LIX

Résumé: Je décrirai comment raisonner en Coq sur des programmes Caml purement fonctionnels, à travers un plongement profond du noyau de Caml dans Coq. Ceci consiste à décrire la syntaxe et la sémantique de Caml à l'aide d'inductifs Coq. On peut ainsi énoncer les spécifications de programmes donnés sous forme de lemmes, puis vérifier ces programmes en prouvant les lemmes de spécification de manière interactive. Cette approche a le bénéfice de n'imposer quasiment aucune restriction sur le code, et de disposer d'un langage de spécification et de preuve extrêmement riche à moindre frais. On verra que cette technique permet de certifier des programmes Caml complexes avec des scripts de longueur assez raisonnable. Pour finir, on discutera de la possibilité de définir une fonction logique Coq à partir du code certifié d'une fonction Caml (le processus inverse de l'extraction).

Liens: Les transparents de l'exposé.