Extraction de programmes dans le Calcul des Constructions
Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité modifiée est introduite et étudiée. Un codage imprédicatif d'une large classe de définitions inducti...
| Main Author: | |
|---|---|
| Language: | FRE |
| Published: |
Université Paris-Diderot - Paris VII
1989
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00431825 http://tel.archives-ouvertes.fr/docs/00/43/18/25/PDF/new.pdf |