Comparing cubes of typed and type assignment systems

Abstract : We study the cube of type assignment systems, as introduced in [10], and confront it with Barendregt's typed λ-cube [3]. The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular , we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that this property holds only for the systems without polymorphism. The type assignment systems we consider satisfy the properties 'subject reduction' and 'strong normalization'. Moreover, we define a new type assignment cube that is isomorphic to the typed one.
Type de document :
Article dans une revue
Annals of Pure and Applied Logic, Elsevier Masson, 1997, 86 Issue 3, pp.267-303. 〈Elsevier〉. 〈10.1016/S0168-0072(96)00036-X〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01154638
Contributeur : Luigi Liquori <>
Soumis le : vendredi 22 mai 2015 - 16:00:47
Dernière modification le : jeudi 11 janvier 2018 - 16:37:57
Document(s) archivé(s) le : jeudi 20 avril 2017 - 07:14:17

Fichier

1997-jpal-07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Steffen Van Bakel, Luigi Liquori, Simona Ronchi Della Rocca, Pawel Urzyczyn. Comparing cubes of typed and type assignment systems. Annals of Pure and Applied Logic, Elsevier Masson, 1997, 86 Issue 3, pp.267-303. 〈Elsevier〉. 〈10.1016/S0168-0072(96)00036-X〉. 〈hal-01154638〉

Partager

Métriques

Consultations de la notice

522

Téléchargements de fichiers

48