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

Frank Pfenning fp at cs.cmu.edu
Mon Jan 28 19:23:15 EST 2013

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.

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

  - 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

More information about the Types-list mailing list