[TYPES] normalization and programming languages

[Thorsten Altenkirch]

Gerard Boudol wrote:

>  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.

If a program is a solution to a problem than knowing that it terminates 
for any input is an important aspect of it being a solution. Often the 
best way to see that it is terminating is expressing it in a language 
where all programs terminate. The programming language Epigram is an 
example of an experimental language which is intended to be terminating 
(even though not all conditions are enforced in the current version), see
http://www.e-pig.org/
for more information.

Since Epigram has dependent types knowing that all terms are terminating 
has other important consequences, not only do we need it to ensure that 
the type checker terminates (practically not so important) but also that 
we allowed to ignore terms which don't carry any computational 
information at runtime. A typical example for those are proofs of 
equalities which are used for coercions. E.g. if you have a vector of 
length m+n but you need one of length n+m you can coerce on to the other 
using a proof that m+n=n+m but you are only allowed to ignore this proof 
at runtime, if you know that it is terminating.

I guess it depends what you mean by "programming language", those of the 
past or those of the future? And what is the fundamental difference 
between a programming language and a language for theorems, once we have 
understood propositions as types?

Cheers,
Thorsten

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.