[TYPES] normalization and programming languages
akenn at microsoft.com
Wed Nov 16 15:22:38 EST 2005
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).
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]
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.
More information about the Types-list