[TYPES] normalization and programming languages

[Joe Wells]

Gerard Boudol <Gerard.Boudol at sophia.inria.fr> writes:

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

There has been interest in type-based guarantees of time complexity
for programming languages, but I don't know of any case where mere
termination without a nice complexity bound has been justified as
interesting.  I think I saw an unpublished paper once claiming this as
a feature, but I failed to grasp the motivation.

> I understand that this result is fundamental for theorem provers,
> where it ensures the consistency of reasoning,

Just curious: Is there any case where _strong_ normalization is needed
for proving consistency of a logic and (weak) normalization is
insufficient?

Similarly, I know that in _some_ theorem proving contexts strong
normalization has been stated to be important because it ensures that
convertibility can be checked by simply reducing to normal form
following any strategy, but it seems to me that knowing a normalizing
strategy is what is really important.

> but I don't immediately see a use of it regarding programming
> languages.

Same for me.

-- 
Joe