|
 
|
[DDT13] RelExt : Synthèse de code à partir de spécifications inductives
Conférence Nationale avec comité de lecture : AFADL 2013, April 2013, pp.4 pages, Nancy, France,
motcle:
Résumé:
Dans ce papier, nous décrivons l’outil RelExt, qui permet de générer du code
fonctionnel à partir de spécifications inductives Coq. Cet outil est capable de produire
deux types de sorties différentes. La première est une sortie ML, obtenue grâce
à une extension du mécanisme natif d’extraction de Coq aux relations inductives. La
deuxième sortie est une sortie Coq, où le code fonctionnel généré est accompagné
des théorèmes et preuves de correction correspondants. Nous présentons également
quelques exemples illustrant ces deux types de sortie.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| DDT13, | |||
| title | = | "{RelExt : Synthèse de code à partir de spécifications inductives }", | |
| author | = | " D. Delahaye and C. Dubois and P. Tollitte ", | |
| booktitle | = | "{AFADL 2013}", | |
| year | = | 2013, | |
| month | = | "April", | |
| pages | = | "4 pages", | |
| address | = | "Nancy, France", | |
| } | |||
