[TYPES] normalization and programming languages

[Yong Luo]

Hi,

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.

Yong
==============================
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]

Hi,

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