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

Paper: 2nd-order unification and type inference for Church-style polymorphism


Hi,

I am pleased to inform you that my paper 

Second-order unification and type inference for Church-style
polymorphism

is available via anonymous ftp from zls.mimuw.edu.pl (file
pub/alx/simple.dvi.gz).

Comments are welcome.

Here is a brief abstract

  We present a proof of the undecidability of type inference for the
  Church-style system ${\cal F}$. For this, we consider the
  second-order unification problem. The natural reduction from
  unification to type inference leads to certain, quite strong,
  restriction on instances --- arguments of variables cannot contain
  variables.  This requires another proof of the undecidability of the
  second-order unification since known results use variables in
  arguments of other variables.  We give such a proof in the present
  paper. Moreover, our proof uses elementary techniques, which is
  important from the methodological point of view, because the
  Goldfarb's proof highly relies on the undecidability of the tenth
  Hilbert's problem. 


Sincerely yours,
Aleksy Schubert