[TYPES] proofs of strong normalization for System F

[Wojtek Moczydlowski]

It'd be nice to have a family of natural type systems corresponding to the 
important subsystems of second-order arithmetics described in the 
Simpson's book.

Wojtek

On Tue, 14 Jul 2009, Thorsten Altenkirch wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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.
>