Math 788 — Fall 2001 Topics in Applied Logic: Typed and Untyped Lambda Calculus

We will examine the syntax, semantics and pragmatics of various lambda calculi as well as applications to the foundations of programming languages.

Alonzo Church originally defined lambda calculus in the 1930s. The untyped version was the salvageable part of an inconsistent, universal "System of Logic," which he had proposed. Church then when on to define the typed lambda calculus which was the backbone of his elegant version of the simple theory of types. Both of these calculi and their extensions have been amazingly influential in recursion theory and computer science. On the theoretical side, Church's Thesis, which identifies intuitive computability with a precise technical notion, was formulated for the lambda calculus. More recently, the lambda calculus has been used to provide a natural framework in which to discuss generalized recursion theory. On the practical side, the Lisp programming language, one of the most long-lived of programming languages, owes its power to its direct appropriation of features from the untyped lambda calculus. The typed lambda calculus, on the other hand, is the ancestor of all typed functional languages. It is the Mother of Functional Programming.

The course will be based on chapters from a forthcoming book by Nerode, Odifreddi, and Platek.