Lambda Calculus and Types

Overview

As a language for describing functions, any literate computer scientist would expect to understand the vocabulary of the lambda calculus. It is folklore that various forms of the lambda calculus are the prototypical functional programming languages, but the pure theory of the lambda calculus is also extremely attractive in its own right. This course introduces the terminology and philosophy of the lambda calculus, and then covers a range of self-contained topics studying the language and some related structures. Topics covered include the equational theory, term rewriting and reduction strategies, combinatory logic, Turing completeness and type systems. As such, the course will also function as a brief introduction to many facets of theoretical computer science, illustrating each (and showing the connections with practical computer science) by its relation to the lambda calculus.

There are no prerequisites, but the course will assume familiarity with construting mathematical proofs. Some basic knowledge of computability would be useful for one of the topics (the Models of Computation course is much more than enough), but is certainly not necessary.

Learning Outcomes

The course is an introductory overview of the foundations of computer science with particular reference to the lambda-calculus. Students will

• understand the syntax and equational theory of the untyped lambda-calculus, and gain familiarity with manipulation of terms;
• be exposed to a variety of inductive proofs over recursive structures;
• learn techniques for analysing term rewriting systems, with particular reference to b-reduction;
• see the connections between lambda-calculus and computabilty, and an example of how an undecidability proof can be constructed;
• see the connections and distinctions between lambda-calculus and combinatory logic;
• learn about simple type systems for the lambda-calculus, and how to prove a strong normalization result;
• understand how to deduce types for terms, and prove correctness of a principal type algorithm.