Documentation Documentation
Identifiant IdRef : 22662871X
Notice de type Rameau

Point d'accès autorisé

Informations

Langue d'expression : Francais
Date de naissance :  2007
Note publique d''information : 
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

Note publique d''information : 
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

Notices d'autorité liées

Autres identifiants

Utilisation dans Rameau

Le point d'accès peut être employé dans un point d'accès sujet

... Références liées : ...