Foundations of Functional Programming

Lecturer: Dr A.N. Other

No. of lectures: 12

This course is a prerequisite for Types (Part II) and is useful for Communicating Automata and Pi Calculus (Part II).

Last year's course is described below. Details of this year's course 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:

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.).