[TYPES] normalization and programming languages

Rene Vestergaard vester at jaist.ac.jp
Wed Nov 16 10:26:49 EST 2005

> I understand that [SN] is fundamental for theorem provers, where it 
> ensures the consistency of reasonning,

It may be worth pointing out that constructive weak normalisation 
suffices for consistency.

It may also be worth pointing to a related discussion on the rewriting 
and proof-theory mailing lists back in Feb (and Jan) 2004 that is 
archived, e.g., here: https://listes.ens-lyon.fr/wws/arc/rewriting


More information about the Types-list mailing list