Computer LaboratoryComputer Science Syllabus - Foundations of Functional Programming

Foundations of Functional Programming
Next: Semantics of Programming Languages Up: Lent Term 2006: Part Previous: Digital Communication I   Contents

Foundations of Functional Programming

Lecturer: Dr A.C. Norman

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

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