[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]>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 >
