[TYPES] proofs of strong normalization for System F

[Matthias Blume]

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