[TYPES] normalization and programming languages

Gerard Boudol Gerard.Boudol at sophia.inria.fr
Wed Nov 16 02:50:07 EST 2005


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

More information about the Types-list mailing list