Intersection-types à la Church

Abstract : 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.
Type de document :
Article dans une revue
Journal of Information and Computation, Elsevier, 2007, 205 (9), pp.1371-1386. 〈10.1016/j.ic.2007.03.005〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01148282
Contributeur : Luigi Liquori <>
Soumis le : lundi 4 mai 2015 - 13:04:18
Dernière modification le : samedi 27 janvier 2018 - 01:31:34
Document(s) archivé(s) le : mercredi 19 avril 2017 - 14:22:32

Fichier

2007-ic-07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

163

Téléchargements de fichiers

50