[TYPES] normalization and programming languages

[Pawel Urzyczyn]

On Wednesday 16 of November 2005 08:50, Gerard Boudol wrote:
> 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.
------------------
I think the moral sense of strong normalization is that a program 
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like 
iteration, recursion etc. My favourite example here is that the 
"big Omega" can be written in Algol 60, because procedure types 
in this language are not fully specified. 
P. Urzyczyn