Foundations of Functional Programming

Lecturer: Dr P.A. Gardner (pag20@cl.cam.ac.uk)

No. of lectures: 12  

This course will be based on last year's course described below. Further details will be available nearer the time.

Part I.

The Lambda calculus. Introduction. Lambda-terms and conversions. Free and bound variables. Abbreviations. Equality. The Church-Rosser Theorem and its consequences. Normal forms. Encoding data in the lambda-calculus. Representations of the booleans, ordered pairs, natural numbers (Church numeral system) and lists. Writing recursive functions. Fixed-point combinators Y and Theta, and their use. The lambda-calculus and computation theory. Lambda-definability. The general recursive functions are lambda-definable. Second fixed-point theorem. Unsolvability of halting problem.

Part II.

Implementation methods. Landin's ISWIM language. The interpreted SECD machine. The need for closures. Example. The compiled SECD machine. Combinators and their reductions. An abstraction algorithm. Basic properties of abstraction. Relation to lambda-calculus. The combinators B and C. Turner's abstraction algorithm. Treatment of data structures and recursion. Examples. Implementing the lambda-calculus in ML.

Recommended books:

Paulson, L.C. (1995). Foundations of Functional Programming. Previous lecture notes for Part IB of the Computer Science Tripos.

Gordon, M.J.C. (1988). Programming Language Theory and its Implementation. Prentice-Hall.

Hindley, J.R. & Seldin, J.P. (1986). Introduction to Combinators and Lambda-Calculus. Cambridge University Press.

Barendregt, H.P. (1984). The Lambda Calculus: its Syntax and Semantics. North-Holland.

Paulson, L.C. (1996). ML for the Working Programmer. Cambridge University Press (2nd ed.).