Extraction de Coq vers Java
Le système Coq, développé par le projet Coq
[1],
est un assistant de preuve formelle qui permet en autres choses de formaliser
des algorithmes et de prouver leurs propriétés (exemples
).
Cette problématique de certification d'algorithmes est au coeur
du nouveau projet ``Lemme'' en cours de formation à l'INRIA Sophia
(Lemme est issu du projet CROAP).
Le système Coq a la particularité d'offrir une traduction
automatique (appelée ``extraction'') en ocaml: un algorithme exprimé
dans le langage de Coq (le calcul des constructions
inductives), donc à un niveau abstrait proche de l'écriture
mathématique, est ainsi traduit automatiquement dans un langage
fonctionnel (ocaml), lui-même compilé en code natif. On
dispose alors d'une implémentation efficace et certifiée
de l'algorithme écrit et prouvé en Coq.
Le but du stage est de réaliser cette traduction automatique
vers Java. Les points importants de ce travail sont:
l'implémentation en Java d'un évaluateur
de calcul avec pattern-matching et récurseur (donc de fermetures
- une fonction plus son contexte d'évaluation -). Ce sera le langage
objet de l'extraction.
l'extension à tout le calcul des
constructions du processus d'extraction, qui dans la version actuelle de
Coq, est restreint aux sortes Prop et Set. On se basera sur les travaux
effectués en ce sens dans l'action coopérative CFC
.C'est
la partie théorique du stage.
la modularité du code Java extrait, qui devrait
pouvoir s'insérer facilement dans d'autres développements
Java. p
pour valider ce stage, on testera l'efficacité de l'extraction
en Java sur des algorithmes pris parmi ceux qui sont déja écrits
et prouvés en Coq ( voir
les contributions CFC , ou bien les deux autres stages sur la
certification de programmes proposés par le projet LEMME).
Encadrement:
Loïc
Pottier
Contact:
Tel: 04 92 38 78 19
E-mail : Loic.Pottier@sophia.inria.fr
Laboratoire d'accueil:
Avant-projet LEMME,
INRIA
Sophia Antipolis
Matériel:
Station de travail ou PC
Durée:
3 mois
Références
[1] G. Huet, G. Kahn, C. Paulin-Mohring, The
Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA
0204, août 1997.
Retour à
la page du projet