[LA] ================================================ AMAST Links 02 04

         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 assignment systems
we consider still have the good computational properties like subject
reduction and strong normalization. 
  Moreover, we define two new type assignment cubes that are isomorphic
to the typed one.

  The paper is available by ftp in two forms, both compressed:
DVI (?=dvi) and PostScript (?=ps) respectively at URL:
ftp://pianeta.di.unito.it/pub/LAMBDA/ronchi/cubes.?.Z