[TYPES] proofs of strong normalization for System F

[Andrei Popescu]

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