Abstract

We study the cube of type assignment systems, as introduced in Giannini-et.al'93. This cube is obtained from Barendregt's typed lambda-cube Barendregt'91 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.

Appeared as:

@Inproceedings {Bakel-et.al-LFCS'94,

Author = "S. van Bakel and L. Liquori and {Ronchi della Rocca}, R. and P. Urzyczyn",
Title = "Comparing {C}ubes",
Booktitle = "Proceedings of LFCS '94. Third International Symposium on Logical Foundations of Computer Science, {\rm St.~Petersburg, Russia}",
Editor = "A. Nerode and Yu. V. Matiyasevich",
Series = "Lecture Notes in Computer Science",
Volume = "813",
Publisher = "Springer-Verlag",
Year = "1994",
Pages = "353-365"
}