Modern functional programming languages such as Haskell, ML (and its successors - SML, Ocaml, F#), Agda2, etc, are equipped with rather rich and complex type systems. Despite this diversity, these systems are based on strong foundation of formal theory of typed lambda calculi.

The course is dedicated to the different systems of typed lambda calculi. The concept of a type is introduced for the pure simply typed lambda-calculus. The Curry-style and Church-style approaches to a typed lambda calculus are examined. The following systems will be discussed: polymorphic types (system F), type operators, higher-order polymorphism, dependent types, recursive types. For these systems the problems of type checking, type assignment (synthesis) and type inhabitation are examined. The correspondence between different logical and type systems is discussed.