[TYPES] normalization and programming languages
jf at cl.cam.ac.uk
Wed Nov 16 10:43:07 EST 2005
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:
,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 Fairbairn Jon.Fairbairn at cl.cam.ac.uk
More information about the Types-list