Skip to Main content Skip to Navigation
Journal articles

Comparing cubes of typed and type assignment systems

Abstract : We study the cube of type assignment systems, as introduced in [10], and confront it with Barendregt's typed λ-cube [3]. The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular , we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that this property holds only for the systems without polymorphism. The type assignment systems we consider satisfy the properties 'subject reduction' and 'strong normalization'. Moreover, we define a new type assignment cube that is isomorphic to the typed one.
Keywords : APAL
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Friday, May 22, 2015 - 4:00:47 PM
Last modification on : Monday, October 25, 2021 - 6:50:36 PM
Long-term archiving on: : Thursday, April 20, 2017 - 7:14:17 AM


Files produced by the author(s)




Steffen van Bakel, Luigi Liquori, Simona Ronchi Della Rocca, Pawel Urzyczyn. Comparing cubes of typed and type assignment systems. Annals of Pure and Applied Logic, Elsevier Masson, 1997, 86 Issue 3, pp.267-303. ⟨10.1016/S0168-0072(96)00036-X⟩. ⟨hal-01154638⟩



Les métriques sont temporairement indisponibles