[TYPES] normalization and programming languages

[Gerard Boudol]

Hi,

I think the TYPES list is the relevant one to ask the following question:

does anyone know an application, or simply a use, in the area of 
programming language semantics, of the classical strong normalization 
result in typed lambda-calculi - for various notions of type? I 
understand that this result is fundamental for theorem provers, where it 
ensures the consistency of reasonning, but I don't immediately see a use 
of it regarding programming languages.

Thanks in advance for your answers.

Gérard Boudol