[TYPES] proofs of strong normalization for System F

[Lorenzo Tortora de Falco]

I would like to mention the recent joint work with Michele Pagani:

Michele Pagani, Lorenzo Tortora de Falco "Strong normalization property
for second order linear logic" to appear in Theoretical Computer Science

available on my web page: http://logica.uniroma3.it/~tortora/

The proof we give uses Girard's method to prove Weak Normalization
(there is absolutely nothing new here), but to infer Strong
Normalization we need what is called in different ways in the
litterature: "conservation theorem" in lambda-calculus see Barendregt's
book for example, "standardization theorem" by Girard and also
"propriété de striction" by Danos. The proof of this result is rather
delicate for full LL: it is the main point of the paper and it is purely
combinatorial.


Lorenzo.


Il giorno mar, 14/07/2009 alle 21.24 +0200, Andrei Popescu ha scritto:

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