[TYPES] proofs of strong normalization for System F

[Derek Dreyer]

Yes, but the core of McAllester et al.'s proof still involves Girard's
method of interpreting a polymorphic type by universal quantification
over an arbitrary set.

Derek

On Tue, Jul 14, 2009 at 9:18 PM, Matthias Blume<blume at tti-c.org> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> There is a 1995 paper in Information and Computation by McAllester,
> Kucan, and Otth titled "A Proof of Strong Normalization of F_2,
> F_omega and Beyond".  It seems to be somewhat different from the
> original Girard proof, but I have not checked the details.
>
> Matthias
>
> On Jul 14, 2009, at 1:38 PM, Derek Dreyer wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>>  ]
>>
>> Andrei,
>>
>> I would refer you to Jean Gallier's article, 'On Girard's "Candidats
>> De Reductibilité"', from the Odifreddi volume of Logic and Computer
>> Science, 1990, but perhaps you already know of it.  It is available
>> here:
>>
>> http://repository.upenn.edu/cgi/viewcontent.cgi?article=1739&context=cis_reports
>>
>> The article presents a number of different variations on Girard's
>> proof, such as typed vs. untyped formulations of the logical relation,
>> in great detail.  It also covers the proof of strong normalization for
>> F-omega.
>>
>> I'm not aware of any proof that departs significantly from Girard's
>> original idea.
>>
>> Best regards,
>> Derek
>>
>>
>> On Tue, Jul 14, 2009 at 8:16 PM, Andrei Popescu<uuomul at yahoo.com>
>> wrote:
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>>>  ]
>>>
>>>
>>>
>>> Hello,
>>>
>>>
>>>
>>> I would like to learn about different proofs of strong
>>> normalization for System F and related systems (featuring
>>> impredicativity), and also about formalizations of such proofs.  In
>>> particular, I am curious if there are any proofs that depart
>>> significantly from Girard's original proof idea.
>>>
>>>
>>>
>>> Thank you in advance for any help with this,
>>>
>>>    Andrei Popescu
>>>
>>>
>>>
>>>
>>>
>
>