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.
Cite
CITATION STYLE
van Bakel, S., Liquori, L., Rocca, S. R. D., & Urzyczyn, P. (1994). Comparing cubes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 813 LNCS, pp. 353–365). Springer Verlag. https://doi.org/10.1007/3-540-58140-5_33
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
