Lambda calculus was proposed by Church as a syntactic system for manipulating constructive notion of functions. Its simplicity and expressive power is remarkable. It also gives rise to questions such as self application and non-termination of reductions. Types are used to annotate terms with more tractable properties. Many type systems, such as simple types, intersection types and polymorphic types have been studied these also relate to types in programming languages. Extensions of lambda calculs are often used to give operational semantics of theoretical core of various programming languages.
Semanics (or model) of lambda calculus, using traditional sets was challenging as it requires embedding a suitable function space over a set D witin D so that function abstraction and applications are definable. Several models were proposed, finally a satisfactory model D1 was found, as a limit of some finite constructions, whose elements have computational significance. This led to development of domain theory, which is also used as a foundation for a theory of computation and semantics of programming languages.
In the course, we will look at these ideas. The course will be theoretical and plans to follow the following text closely.
[1] J.L.Krivine, Lambda-Calculus, Types and Models, Ellis Horwood Series in Computers and their application, 1990.