[TYPES] normalization and programming languages

[Jon Fairbairn]

On 2005-11-16 at 08:50+0100 Gerard Boudol wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 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.

Back in the mists of time, I used this in the Ponder
compiler to guarantee termination of compile-time reduction
of pieces of programme.  It's in a paper I gave to the lisp
conference.  I think it's this one:


@InProceedings(CODE-GENERATION-TECHNIQUES-FOR-FUNCTIONAL-LANGUAGES
	,Key = "Fairbairn"
	,Author = "Jon Fairbairn and Stuart C. Wray"
	,Title = "Code Generation Techniques for Functional Languages"
	,Pages = "94-104"
	,Booktitle = "Proc.~1986 ACM Conference on Lisp and Functional Programming"
	,Organization = "ACM SIGPLAN/SIGACT/SIGART"
	,Year = "1986"
	,Month = Aug
	,Address = "Cambridge, Massachusetts")


I can't remember much about it though!

 Jón

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk