Return to search

Etude d'un $\lambda$-calcul issu d'une logique classique

Le $\lambda \mu^{\wedge \vee}$-calcul est une extension du $\lambda$-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs.<br>Les principaux résultats de cette thèse sont :<br>- La standardisation, la confluence et une extension de la machin de J.-L. Krivine en $\lambda \mu^{\wedge \vee}$-calcul.<br>- Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures.<br>- Une sémantique de réalisabilité pour le $\lambda \mu^{\wedge \vee}$-calcul qui permet de caractériser le comportement calculatoire de certains termes typés et clos.<br>- Un théorème de complétude pour le $\lambda \mu$-calcul simplement typé.<br>- Une introduction à un $\lambda \mu^{\wedge \vee}$-calcul par valeur confluent.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00415845
Date06 July 2007
CreatorsSaber, Khelifa
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0022 seconds