The lambda calculus is a formal system for studying the definitions of functions, independently of the domains and ranges on which those functions operate. It was invented as a model of the lower-level mechanics of mathematical logic, but today it is mainly applied to the design of control structures for programming languages. Along the way, it provided the first characterization of the computable functions and the foundation for proof theory, and it showed the subtlety of the relation between parallelism and nondeterminism, which is still misunderstood today. This course covers the crucial properties of the lambda calculus and its variable-free cousin the combinator calculus, emphasizing the deep connections between various areas of logic and computation that arise from the ability to interpret a lambda term equally naturally as a program and as a proof. In particular, the pun by which A=>B may denote that A implies B, or the class of functions from A to B, turns out to have a deep significance, leading to intuitive foundations for intuitionism, and radically new and useful ideas of the power of a logical system.

The course is moderately challenging mathematically, at perhaps the level of introductory group theory, but it is especially demanding in the breadth of intuition required to see the fundamental unity of the very different sounding applications of the calculus. The material is essential for computer scientists interested in foundational theory or in programming language design. It is very useful for all graduate students in computer science, and also valuable to college students who have the flexibility to connect mathematical theorems closely to practical and philosophical intuitions.