[TYPES] proofs of strong normalization for System F

[Martin Berger]

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

Hello Andrei, sorry for the late reply.  Another way of proving
termination for System F (under the CBV reduction relation) is to
embed System F in the polymorphic pi-calculus in the following
steps.

a. Take the CBV version of Milner's translation of (untyped)
    lambda-calculus into (untyped) pi-calculus.

b. Translate System F types into polymorphic pi-calculus types.

c. Show that the translation in (a) embeds terms that are typable
    in System F as processes that are typable in the polymorphic
    pi-calculus.

d. Show that whenever a System F term M has a one-step CBV
    reduction then the translation has an n-step reduction in
    the pi-calculus for some n > 0.

e. Show that the polymorphic pi-calculus is strongly normalising.

All steps have been proven in [1], all steps but (e) are
straightforward.  Our proof of (e) is an adaptation of the usual
candidate-method to processes. Although we have not done this in
detail, the choice of CBV does not seem to be fundamental, I believe
a similar development could be done for CBN.

Is our proof departing significantly from Girard's original
proof? I'll leave that to you to decide.

[1] M. Berger, K. Honda, N. Yoshida: Genericity and the Pi-Calculus.
Acta Informatica, Vol. 42(2), pp.83–141, 2005. Available from:
http://www.informatics.sussex.ac.uk/users/mfb21/publications/fossacs03

Martin