[TYPES] proofs of strong normalization for System F

[Derek Dreyer]

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