Computing Publications

Publications Home » Comparing Cubes of Typed and Type...

Comparing Cubes of Typed and Type Assignment Systems

Steffen van Bakel, Luigi Liquori, Simona Ronchi delle Rocca, Pawel Urzyczyn

Journal Article
Annals of Pure and Applied Logic
Volume 86
Issue 3
pp.267–303
July, 1997
Elsevier
DOI 10.1016/S0168-0072(96)00036-X
Abstract

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.

PDF of full publication (237 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.