[TYPES] normalization and programming languages

[Andrew Kennedy]

In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the *classical* SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ). 

- Andrew.

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Gerard Boudol
Sent: 16 November 2005 07:50
To: types at cis.upenn.edu
Subject: [TYPES] normalization and programming languages

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

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