Typed Lambda Calculus

Any of several variants of the LambdaCalculus in which terms have types, and the type of an abstraction term is determined by the type of the variable it abstracts and the type of the expression over which it abstracts, and an abstraction term can only be applied to a term of the abstraction's domain type.

For example, if the type of x is A, and the type of y is B, then the type of \x.y is [A->B], meaning (a) the abstraction can be legally applied only to a term of type A, and (b) when it is so applied, the result has type B.

The introduction of types, and the restriction of application to require type match between the applied abstraction and the applicand, avoids certain antinomic, RussellParadox-y problems, and introduces (when you try to invent terms that represent types, thereby embedding the type system in the language) other TypeOfAllTypes?-y problems.

OTOH, these "RussellParadox-y problems" don't actually result in any theoretical difficulty with the UntypedLambdaCalculus. They just result in divergent computations -- and the possibility of that is inevitable for any TuringComplete model of computation.