Comparing Cubes of Type Systems
Subject: Comparing Cubes of Type Systems
From: firstname.lastname@example.org (Simonetta Ronchi_della_Rocca)
Date: Mon, 6 Mar 95 17:14:48 +0100
The following paper is now avalaible by anonymous ftp:
Comparing Cubes of Typed and Type Assignment Systems
Steffen van Bakel, Luigi Liquori,
Simona Ronchi della Rocca, and Pawel Urzyczyn
We study the Cube of Type Assignment System, obtained from
Barendregt's typed lambda-cube via a natural type erasing
function E, 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. Such a
property is obvious for systems without dependent types, since
there exists a simple isomorphism between derivations.
There is no such isomorphism when dependent types are allowed,
and we show that the above mentioned property holds only for the
systems without polymorphism. On the other hand, the type assign-
ment systems we consider still have the good computational proper-
ties like subject reduction and strong normalization.
Moreover, we define two new type assignment cubes that are iso-
morphic to the typed one.
The paper is avalaible at the following ftp site:
in the following directory:
choosing either one of the files:
cubes.ps.Z (PostScript Compressed)
cubes.dvi.Z (dvi Compressed)
Simona Ronchi della Rocca
Dipartimento di Informatica,
Universita' di Torino,
Corso Svizzera 185,
10149 Torino (Italy)