Programmation fonctionnelle certifiée : <br />L'extraction de programmes dans l'assistant Coq
Nous nous intéressons ici à la génération de programmes certifiés<br />corrects par construction. Ces programmes sont obtenus en<br />extrayant l'information pertinente de preuves constructives réalisées<br />dans l'assistant de preuves Coq.<br /><br />Une tel...
| Main Author: | |
|---|---|
| Language: | FRE |
| Published: |
Université Paris Sud - Paris XI
2004
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00150912 http://tel.archives-ouvertes.fr/docs/00/15/09/12/PDF/these_letouzey.pdf |