[TYPES] normalization and programming languages

Yong Luo Y.Luo at kent.ac.uk
Wed Nov 16 12:52:28 EST 2005


Let's answer a simple question: is M of type A?
For simply typed lambda-calculi, computation (or reduction) is not needed.
So, strong normalisation is not important at all. For example, ML and
Haskell don't require termination.

But for dependently typed lambda-calculi, we need to decide whether two
terms are equal. For example, if M is of type Vector(n) and n is "equal" to
m, then M is of type Vector(m). Strong normalisation is perhaps one of the
key requirements to decide whether n is "equal" to m.

Epigram requires termination. I have implemented a type system which doesn't
check totality but do require termination.

Dr. Yong Luo
Computing Laboratory
University of Kent

----- Original Message ----- 
From: "Gerard Boudol" <Gerard.Boudol at sophia.inria.fr>
To: <types at cis.upenn.edu>
Sent: Wednesday, November 16, 2005 7:50 AM
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.

Gérard Boudol

More information about the Types-list mailing list