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

[Fujita Kenetsu]

Dear Chris,

In some (or many) cases, already known proofs can work for predicative 
versions
of System F as well. You can find one example from the paper with 
Aleksy, as
informed by Frank Pfenning:

http://www.sciencedirect.com/science/article/pii/S0890540112001150
Fujita, Schubert: The undecidability of type related problems in the 
type-free
style System F with finitely stratified polymorphic types,
Information and Computation Vol. 218, pp. 69--87, 2012.

With best regards,

Ken
---
Ken-etsu Fujita
Gunma University

(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.
> 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<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