[TYPES] normalization and programming languages

[François-Régis Sinot]

Barry Jay wrote:
> Another way to put this is that data structures should be definable in a 
> strongly-normalising language so that data access, etc. is guaranteed to 
> terminate.  Then add fixpoints or loops to describe arbitrary computations.

Although it is not exactly the case, as any of the following features
may cause non-termination as well: concrete datatypes, references,
exceptions, objects, etc.
See http://www.lri.fr/~signoles/prog/misc/lambda.ml.html for a nice
series of examples of non-terminating OCaml programs without any "let
rec" or "while".

So I think the morale is that, while normalisation results are useful,
the "classical" SN result is usually not enough.
For instance, theorem provers like Coq use a SN result for a
lambda-calculus enriched with concrete datatypes with some conditions
(calculus of inductive constructions).

So the question is: in a real-world functional language, are there known
and reasonably general techniques to detect SN terms ?

Best,
F-R Sinot.