Now I will give a brief introduction to typed l-calculus. Typed l-calculus arise essentially from Church's simple types.
Here is an example where we have typed to the following function, you see it is a way of decorating l-calculus terms with expressions which give some kind of information on the kind of behaviour of the term.
There're various type languages: the simple types, second order types, introduced in the 80s by Girard and Reynolds. This is really the type discipline which allows a phenomenon called polymorphism.
Here is an example of a generic type or polimorphic type for this expression.
There are yet more powerful typing disciplines, and one of the most interesting is the so called calculus of constructions due to Coquand & Huet. It is a situation where not only you can quantify types, but you can quantify also type constructors of all kinds.