



Next: Programming in C and Up: Lent Term 2009: Part Previous: Floating-Point Computation Contents
Foundations of Functional Programming
Lecturer: Dr M.J. Parkinson
No. of lectures: 12
This course is a prerequisite for Types (Part II).
Aims
This course aims (a) to show how lambda-calculus and related theories can provide a foundation for a large part of practical programming, (b) to present students with one particular type analysis algorithm so that they will be better able to appreciate the Part II Types course, and (c) to provide a bridge between the Part IA Foundations of Computer Science course and the theory options in Part II.
Lectures
- Introduction.
Combinators. Constants and Free Variables. Reduction.
Equality. The Church-Rosser theorem. Normal forms.
[1 lecture]
- 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.
Eager and Lazy evaluation.
[2 lectures]
- Encoding of data. Booleans, tuples, lists and trees, numbers.
The treatment of recursion: the Y combinator and its use.
[2 lectures]
- Implementations of lambda calculus. Conversion from
lambda-calculus to combinators. Combinator reduction as
tree-rewrites. The treatment of lambda-bindings in an interpreter:
the environment. Closures. ML implementation of
lambda-calculus. SECD machine. Brief survey of performance issues.
[3 lectures]
- Relationship between this and Turing computability. The
halting problem etc. [0.5 lecture]
- Modelling imperative programming styles. Handling state
information and the continuation-passing style. Return address seen
as an additional continuation parameter. [2.5 lectures]
- Let-polymorphism reviewed following the Part IA coverage of ML. Unification. A type-reconstruction algorithm. Decidability and potential costs. [1 lecture]
Objectives
At the end of the course students should
- understand the rules for the construction and processing
of combinatory terms and terms in the lambda calculus
- know how to model all major aspects of general-purpose
computation in terms of these primitives
- know how lambda terms may be efficiently interpreted by machine
- be able to derive ML-style type judgements
for languages based upon the lambda-calculus
Recommended reading
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: Programming in C and Up: Lent Term 2009: Part Previous: Floating-Point Computation Contents