Lecturer: Alexander Leitsch
The lambda-calculus was developed around 1934 as tool to formalize the concept of computable functions and to provide a firm foundation to mathematical logic. In more recent times the lambda-calculus proved crucial in the development of functional programming languages (like LISP) and in semantics of programming languages (denotational semantics). Generally the lambda-calculus is a flexible and powerful formalism connecting problems in logic, metamathematics and computer science.
In the course we concentrate mainly on the mathematical foundations of the Lambda calculus. The topics in more detail: syntax, lambda-conversion, beta-reduction, eta-reduction, normal form, confluence and termination, extensionality, the Church-Rosser theorem, lambda-definability, numeral systems, recursive functions, undecidability results. Finally we focus on combinatory logic, and the semantics of the lambda-calculus (combinatory algebras).
The course is based on the textbook The Lambda Calculus from H.P. Barendregt, North Holland, 1985.