[TYPES] proofs of strong normalization for System F

[Thorsten Altenkirch]

My first published paper was about a formalisation of strong  
normalisation for System F,
see http://www.cs.nott.ac.uk/~txa/publ/tlca93.pdf
This proof however followed Girard's proof.

Later we used normalisation by evaluation to construct a normalisation  
function for System F,
see
http://www.cs.nott.ac.uk/~txa/publ/lics96.pdf
and
http://www.cs.nott.ac.uk/~txa/publ/f97.pdf
the latter paper was never published.

As Wojtek remarked all proofs of SN for System F already use  
impredicative reasoning. However, Klaus Aehlig showed in his PhD that  
System F with only one type variable can be shown consistent using  
generalized inductive definitions (ID<w). Afaik, nobody has yet taken  
this up to give a predicative normalisation proof for this fragment.  
Another question is whether there are other (larger) fragments which  
can be attacked with predicative methods.

Cheers,
Thorsten


On 14 Jul 2009, at 19:16, Andrei Popescu 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
>
>
>
>


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.