en fr The $lambda mu^{wedge vee}$-calculus Etude dun $lambda$-calcul issu dune logique classique Reportar como inadecuado




en fr The $lambda mu^{wedge vee}$-calculus Etude dun $lambda$-calcul issu dune logique classique - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LAMA - Laboratoire de Mathématiques

Abstract : The $\lambda \mu^{\wedge \vee}$-calculus is an extension of the $\lambda$-calculus associated to the full classical natural deduction.The main results of this thesis are:- A standardization theorem, the confluence theorem, and an extension of J.-L. Krivine machine to the $\lambda \mu^{\wedge \vee}$-calculus.- A semantical proof of the strong normalization theorem of the cut elimination procedure. - A semantics of realizability for the $\lambda \mu^{\wedge \vee}$-calculus and characterization of the operational behavior of some closed typed terms.- A completeness theorem for the simply typed $\lambda \mu$-calculus.- A confluent call-by-value $\lambda \mu^{\wedge \vee}$-calculus.

Résumé : 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.Les principaux résultats de cette thèse sont :- La standardisation, la confluence et une extension de la machin de J.-L. Krivine en $\lambda \mu^{\wedge \vee}$-calcul.- Une preuve sémantique de la forte normalisation du théorème d-élimination des coupures.- 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.- Un théorème de complétude pour le $\lambda \mu$-calcul simplement typé.- Une introduction à un $\lambda \mu^{\wedge \vee}$-calcul par valeur confluent.

fr it

Mots-clés : forte normalisation calcul par valeur réductions parallèles complétude développements finis standardisation $\lambda$-calcul $\lambda \mu$-calcul

keyword : $\lambda \mu$-calculus standardization confluence finiteness developments strong normalization completeness call-by-value parallel reductions $\lambda$-calculus





Autor: Khelifa Saber -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados