Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il présente, étudie et justifie les choix faits dans le système Coq.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00431817 |
| Date | 13 December 1996 |
| Creators | Paulin-Mohring, Christine |
| Publisher | Université Claude Bernard - Lyon I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | habilitation ࠤiriger des recherches |
Page generated in 0.0016 seconds