**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**