[TYPES] normalization and programming languages

Pawel Urzyczyn urzy at mimuw.edu.pl
Wed Nov 16 12:55:55 EST 2005

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

More information about the Types-list mailing list