Syllabus
Typed lambda calculus. Extension of lambda calculus language with object types. Curry and Church variants of type systems, their axiomatic systems. Böhm trees, head normal form, approximations.
Extensions of Curry type systems with polymorphism, intersection types and recursive types.
Hierarchy of typed lambda calculus theories, lambda cube. Questions of type checking, type derivation, and type inhabitation. Strong normalization. Pure type systems. Relations of type systems with logic.
Annotation
Typed lambda calculi, Curry and Church variants. Extensions of type systems.
Questions of type checking, type derivation, and type inhabitation.