[TYPES] normalization and programming languages
Yong Luo
Y.Luo at kent.ac.uk
Wed Nov 16 12:52:28 EST 2005
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
More information about the Types-list
mailing list