[TYPES] Proofs of strong normalization for system F

[Jean Gallier]

Besides my "Candidats de reductibilite" paper,
in 1995, I attempted to axiomatize the conditions
that make the reducibility method work, not just for
SN, but also other properties such as confluence, in
"Proving properties of lambda-terms using realizability,
covers and sheaves" (TCS, No 142(2), 299-368), also found there:
http://www.cis.upenn.edu/~jean/gbooks/logic.html
(after my old logic book) .
A related attempt is in
"Kripke models and the (in)equational logic of the second-order
lambda-calculus" (Annals of Pure and Applied Logic, 84, 257-316, 1997)
also found in
http://www.cis.upenn.edu/~jean/gbooks/logic.html

Krivine also gives a very clean proof of SN for system F in his book
on the lambda-calculus.

I personally don't feel that the "McAllester proof"  is significantly  
new or illuminating.


Best,
-- Jean Gallier