As I said we would also like to move to other more powerful formal systems, to more powerful typed disciplines. The first choice is to add to our very simple typed structure a notion of quantification over types. In this we get what is usually called the second order l-calculus, or polymorphic l-calculus. This corresponds to second order logic where we quantify also over types, over formulas. Correspondingly we extend the language of types. We have the function type as before, but then we also have quantified types, denoted by this type Pt.T (read: for all t in T"), which corresponds to the functions that take as argument a type and return a value in the type T. Also the terms are extended. We have the first order terms that we already had in the typed l calculus; moreover, we also have these new terms, the red ones on the slide. We have abstractions over types. It is a function that takes first of all a type. Then we have the applications of these functions to a type. Correspondingly, we have these rewriting rules: the left one is a rule for application. We have M, which is a function from types to terms of type A, and we may apply this term M to the type B. The type of the result will be A where B has been substituted for the free occurrences of T. On the other hand, once we have M of type A, we may abstract over the type t. We get that M as type "for all t in A". And correspondingly we have a contraction notion also at the second order level. If we have a second order abstraction applied to a type, we have a reduction, a contraction and the result will be M where A has been substituted for the free occurrences of the variable t.

---