[TYPES] proofs of strong normalization for System F

[Matthias Blume]

Yes, indeed.

Matthias

On Jul 14, 2009, at 2:35 PM, Derek Dreyer wrote:

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