[TYPES] Decidability of type reconstruction in predicative System-F?

[Frank Pfenning]

Hi Chris,

  It depends on exactly how you defined type reconstruction.
For one definition, I proved undecidability for the predicative
case in the paper below, based on a suggestion by Bob Harper.

Frank Pfenning. On the undecidability of partial polymorphic type
reconstruction. Fundamenta Informaticae, 19(1,2):185-199, 1993.
Preliminary version available as Technical Report CMU-CS-92-105, School of
Computer Science, Carnegie Mellon University, January 1992.
http://www.cs.cmu.edu/~fp/papers/CMU-CS-92-105.pdf

Fujita and Schubert have results for other definitions, while
remaining predicative (RTA 2010, with a longer version in I&C 2012).

   Best,
  - Frank


On Mon, Jan 28, 2013 at 5:38 PM, Christian Skalka <wintersmind at gmail.com>wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
> I am wondering if there are formal results related to the (un?)decidability
> of type reconstruction in predicative System-F. As I understand it, Joe
> Wells' well-known undecidability result only applies to impredicative
> System-F.
>
> Pointers/citations appreciated.
>
> Thanks,
>
> -chris
>
> --
> Christian Skalka
> Associate Professor
> Department of Computer Science
> University of Vermont
> http://www.cs.uvm.edu/~skalka
>