Intersection-types à la Church - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Information and Computation Année : 2007

Intersection-types à la Church

Résumé

In this paper, we present Λ^t_∧, a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Λ^t_∧ and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable.
Fichier principal
Vignette du fichier
2007-ic-07.pdf (243.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01148282 , version 1 (04-05-2015)

Identifiants

Citer

Luigi Liquori, Simona Ronchi Della Rocca. Intersection-types à la Church. Information and Computation, 2007, 205 (9), pp.1371-1386. ⟨10.1016/j.ic.2007.03.005⟩. ⟨hal-01148282⟩

Collections

INRIA INRIA2
86 Consultations
154 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More