[ 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
