[Prev][Next][Index][Thread]

Comparing Cubes of Type Systems


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 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:

  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)