<i>Annals of Pure and Applied Logic</i>, 86(3):267-303, 1997

Abstract

Comparing Cubes of Typed and Type Assignment Systems.
by S. van Bakel, L. Liquori, R. Ronchi della Rocca, and P. 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.

Appeared as:
@Article {Bakel-et.al-APAL'97,
Author = "S. van Bakel and L. Liquori and {Ronchi Della Rocca}, S. and P. Urzyczyn",
Title = "Comparing {C}ubes of {T}yped and {T}ype {A}ssignment {S}ystems",
Journal = "Annals of Pure and Applied Logic",
Volume = "86",
Year = "1997",
Pages = "267-303"
}

ps pdf