Etude d’un Lambda-calcul issu d’une logique classique
Institution:
ChambéryDisciplines:
Directors:
Abstract EN:
The lmÙÚ-calculus is an extension of the l-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. -1. Krivine machine to the lmÙÚ-calculus. -A semantical proof of the strong normalization theorem of the cut elimination procedure. -A semantics of realizability for the lmÙÚ-calculus and characterization of the operational behavior of some closed typed terms. -A completeness theorem for the simply typed lm-calculus. -A confluent call-by-value lmÙÚ-calculus
Abstract FR:
Le llm ÙÚ- calcul est une extension du l-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 machine de J. -L. Krivine en lmÙÚ-calcul. -Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures. -Une sémantique de réalisabilité pour Ie calcul qui permet de caractériser Ie comportement calculatoire de certains termes types. -Un théorème de complétude pour Ie lmÙÚ-calcul simplement typé. -Une introduction et un lmÙÚ-calcul par valeur confluent