[TYPES] Decidability of type reconstruction in predicative System-F?
fujita at cs.gunma-u.ac.jp
Tue Feb 12 08:06:53 EST 2013
In some (or many) cases, already known proofs can work for predicative
of System F as well. You can find one example from the paper with
informed by Frank Pfenning:
Fujita, Schubert: The undecidability of type related problems in the
style System F with finitely stratified polymorphic types,
Information and Computation Vol. 218, pp. 69--87, 2012.
With best regards,
(2013/01/29 9:23), Frank Pfenning wrote:
> [ 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.
> 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
>> Pointers/citations appreciated.
>> Christian Skalka
>> Associate Professor
>> Department of Computer Science
>> University of Vermont
More information about the Types-list