typed lambda-calculus
<theory> (TLC) A variety of {lambda-calculus} in which every
term is labelled with a {type}.
A {function application} (A B) is only synctactically valid if
A has type s --> t, where the type of B is s (or an {instance}
or s in a {polymorphic} language) and t is any type.
If the types allowed for terms are restricted, e.g. to
{Hindley-Milner types} then no term may be applied to itself,
thus avoiding one kind of non-terminating evaluation.
Most {functional programming} languages, e.g. {Haskell}, {ML},
are closely based on variants of the typed lambda-calculus.
(1995-03-25)