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 inductives est proposé.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00431825 |
| Date | 27 January 1989 |
| Creators | Paulin-Mohring, Christine |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0031 seconds