[Prev][Next][Index][Thread]
Comparing Cubes of Type Systems

To: types@dcs.gla.ac.uk

Subject: Comparing Cubes of Type Systems

From: ronchi@di.unito.it (Simonetta Ronchi_della_Rocca)

Date: Mon, 6 Mar 95 17:14:48 +0100

Approved: types@dcs.gla.ac.uk
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
ABSTRACT
We study the Cube of Type Assignment System, obtained from
Barendregt's typed lambdacube 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:
pianeta.di.unito.it
in the following directory:
/pub/LAMBDA/ronchi
choosing either one of the files:
cubes.ps.Z (PostScript Compressed)
cubes.dvi.Z (dvi Compressed)
Simona.
Address:
Simona Ronchi della Rocca
Dipartimento di Informatica,
Universita' di Torino,
Corso Svizzera 185,
10149 Torino (Italy)