Return to search

Définitions Inductives en Théorie des Types

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.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00431817
Date13 December 1996
CreatorsPaulin-Mohring, Christine
PublisherUniversité Claude Bernard - Lyon I
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
Typehabilitation ࠤiriger des recherches

Page generated in 0.0017 seconds