[TYPES] proofs of strong normalization for System F

[Ralph Loader]

Andrei,

Once upon a time I gave a proof based on functional interpretations.

See http://homepages.ihug.co.nz/~suckfish/papers/normal.pdf

Given a term, I derive another term that calculates the size of the
normalisation tree of the first.

Then a model (or weak normalisation for that matter) can be used to
verify correctness of the calculation; the condition on the model to
make this work is essentially just that some type correctly represents
the natural numbers.

All the impredicativity is pushed back into the model, the syntactical
constructions are all primitive recursive.

Cheers,
Ralph.


On Tue, 14 Jul 2009 11:16:11 -0700 (PDT)
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 
> 
> 
> 
>