Return to search

un lambda calcul intuitioniste avec exceptions

La thèse décrit un lambda calcul typé étendu par un traitement des exceptions. Ses principales propriétés sont : confluence, forte normalisation, conservation du type (dans une forme parallélisée de réduction). Seuls les termes équivalents aux entiers de Church ont le type entier. La comparaison avec le système d'exceptions du langage Caml est développée. Mais le plus remarquable est que la logique du système n'est pas la logique classique mais la logique intuitionniste.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00093187
Date19 February 1999
CreatorsMounier, Georges
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0019 seconds