Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Wednesday, May 27, 2015 - 5:30:07 PM
Last modification on : Wednesday, June 23, 2021 - 3:14:03 PM
Long-term archiving on: : Monday, April 24, 2017 - 4:49:24 PM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles