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.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00415845 |
| Date | 06 July 2007 |
| Creators | Saber, Khelifa |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds