[TYPES] Decidability of type reconstruction in predicative System-F?
fp at cs.cmu.edu
Mon Jan 28 19:23:15 EST 2013
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).
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
> Pointers/citations appreciated.
> Christian Skalka
> Associate Professor
> Department of Computer Science
> University of Vermont
More information about the Types-list