Des preuves de totalite de fonctions comme synthese de programmes
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
Les travaux de theorie de la demonstration axes sur le lambda-calcul type nous donnent la possibilite de construire des systemes de synthese de programmes a partir de preuves formelles de specifications. L'interet des systemes developpes dans ce contexte est que les programmes qui y sont obtenus sont corrects. Les auteurs de cette these utilisent un systeme de lambda-calcul type dans lequel, pour obtenir un programme qui calcule une fonction, il suffit de prouver que celle-ci est totale sur son domaine. Apres avoir presente le cadre general dans lequel ils travaillent (la theorie de types recursifs), les auteurs proposent une methode de preuve par recurrence pour les enonces de totalite de fonctions equationnellement definies. Ils donnent ensuite deux strategies automatiques de recherche de preuves conformes a cette methode et demontrent que toutes deux sont correctes et completes. La difference essentielle entre ces deux strategies est le principe de recurrence utilise. Autour de ces strategies, les auteurs ont implemente un systeme de programmation par preuve se presentant comme un langage de programmation fonctionnelle