Source : Free On-Line Dictionary of Computing

typed lambda-calculus
     
         (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)