Steffen van Bakel, Luigi Liquori, Simona Ronchi delle Rocca, Pawel Urzyczyn
We study the Giannini-Honsell-Ronchi `cube of type assignment systems', and confront it with Barendregt's typed lambda-cube. 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.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.