Comparing Cubes - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 1994

Comparing Cubes

Résumé

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.
Fichier principal
Vignette du fichier
1994-lfcs-94.pdf (305.55 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01157211 , version 1 (27-05-2015)

Identifiants

Citer

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. pp.353-365, ⟨10.1007/3-540-58140-5_33⟩. ⟨hal-01157211⟩

Collections

INRIA INRIA2
164 Consultations
82 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More