[TYPES] normalization and programming languages

[Rene Vestergaard]

> 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

Cheers,
/R