*Lecturer: Dr A.C. Norman*
(`acn1@cl.cam.ac.uk`)

*No. of lectures:* 12

*This course is a prerequisite for Types (Part II).*

**Aims**

- To show how lambda-calculus and related theories can provide a
foundation for a large part of practical programming.
- To present students with one particular type analysis algorithms
so that they will be better able to appreciate the Part II
*Types*course. - To provide a bridge between the Part IA
*Foundations of Computer Science*course and the theory options in Part II.

Part A. The theory

- Introduction. Combinators. Constants and Free Variables. Reduction.
Equality. the Church-Rosser theorem. Normal forms.
- The Lambda calculus. Lambda-terms, alpha and beta conversions.
Free and bound variables. Abbreviations in the notation.
Pure and applied lambda calculi. Relationship
between combinators, lambda calculus and typical programming languages.
- Encoding of data: booleans, tuples, lists and trees, numbers.
The treatment of recursion: the
*Y*combinator and its use. - Modelling imperative programming styles: handling state information
and the continuation-passing style.
- Relationship between this and Turing computability, the halting problem etc.

Part B. Implementation techniques

- Combinator reduction as tree-rewrites. Conversion from lambda-calculus to
combinators. The treatment of lambda-bindings
in an interpreter: the
*environment*. Closures. ML implementation of lambda-calculus. SECD machine. Brief survey of performance issues.

Part C. Type reconstruction

- Let-polymorphism reviewed following the Part IA coverage
of ML. Unification. A type-reconstruction algorithm. Decidability and
potential costs.

**Objectives**

At the end of the course students should

- understand the rules for the construction and processing
of terms in the lambda calculus and of Combinators
- know how to model all major aspects of general-purpose
computation in terms of these primitives
- be able to derive ML-style type judgements
for languages based upon the lambda-calculus

**Recommended books**

Hindley, J.R. & Seldin, J.P. (1986). *Introduction to Combinators and
Lambda-Calculus*. Cambridge University Press (now out of print but try a
library).

Revesz, G.E. (1988). *Lambda Calculus, Combinators and Functional
Programming*. Cambridge University Press (now out of print but try a library).