Next: Project Briefing I
Up: Easter Term 2003: Part
Previous: Databases
  Contents
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).
Next: Project Briefing I
Up: Easter Term 2003: Part
Previous: Databases
  Contents
Christine Northeast
Wed Sep 4 14:43:05 BST 2002