Comparing Cubes

Abstract : We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt's typed λ-cube [1] via a natural type erasing function E, that erases type information from terms. We prove that the systems in the former cube enjoy good computational properties, like subject reduction and strong normalization. We study the relationship between the two cubes, which leads to some unexpected results in the field of systems with dependent types.
Type de document :
Communication dans un congrès
Logical Foundations of Computer Science. Third International Symposium, LFCS '94 St. Petersburg, Russia, July 11–14, 1994 Proceedings, Jul 1994, St. Petersburg, Russia. Springer Verlag, 813, pp.353-365, Lecture Notes in Computer Science. 〈10.1007/3-540-58140-5_33〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01157211
Contributeur : Luigi Liquori <>
Soumis le : mercredi 27 mai 2015 - 17:30:07
Dernière modification le : jeudi 11 janvier 2018 - 16:41:02
Document(s) archivé(s) le : lundi 24 avril 2017 - 16:49:24

Fichier

1994-lfcs-94.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Steffen Van Bakel, Luigi Liquori, Simona Ronchi Della Rocca, Pawel Urzyczyn. Comparing Cubes. Logical Foundations of Computer Science. Third International Symposium, LFCS '94 St. Petersburg, Russia, July 11–14, 1994 Proceedings, Jul 1994, St. Petersburg, Russia. Springer Verlag, 813, pp.353-365, Lecture Notes in Computer Science. 〈10.1007/3-540-58140-5_33〉. 〈hal-01157211〉

Partager

Métriques

Consultations de la notice

162

Téléchargements de fichiers

45