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

Type reconstruction in F_\omega




A revised full version of my paper 
                 Type reconstruction in F_\omega
is now available by anonymous ftp from:

ftp.mimuw.edu.pl
directory /pub/users/urzy
files fomega.ps.Z fomega.dvi.Z

cs-ftp.bu.edu
directory /urzy
files fomega.ps fomega.dvi

Abstract
We investigate the Girard's calculus F_\omega as a ``Curry style'' type 
assignment system for pure lambda terms. First we show an example of a 
strongly normalizable term that is untypable in F_\omega. Then we prove 
that every partial recursive function is non-uniformly represented in 
F_\omega (even if quantification is restricted to constructor variables 
of rank 1). It follows that the type reconstruction problem is undecidable 
and cannot be recursively separated from normalization.

Pawe{\l} Urzyczyn