Course Catalogue

View Specification Document | Reading List

This course covers the theory of sequential and concurrent computation. The main topics include the lambda calculus as a foundation for functional computation and the pi calculus as a foundation for concurrent computation; the theory of operational semantics and type systems for both these calculi.

2 hours of lecture time and 1 hour of tutorial or practical work per week

None

None

None

80% for the end of year exam

20% for assessed coursework, which is will be one single assignment

The assessed coursework will assess ILOs 1, 4, 7 and 8 as well as touching on other ILOs.

The exam will assess ILOs 1, 2, 3, 5, 6.

Reassessments are normally available for all courses, except those which contribute to the Honours classification. For non-Honours courses, students are offered reassessment in all or any of the components of assessment if the satisfactory (threshold) grade for the overall course is not achieved at the first attempt. This is normally grade D3 for undergraduate students and grade C3 for postgraduate students. Exceptionally it may not be possible to offer reassessment of some coursework items, in which case the mark achieved at the first attempt will be counted towards the final course grade. Any such exceptions for this course are described below. 

The nature of the coursework is such that it takes a significant number of days to produce it and this effort is infeasible for supporting the re-doing of such coursework over the summer.

The aim of the course is to show how these two models of computation can be formally defined in order to give a rigorous foundation for sequential and concurrent programming paradigms.

By the end of this course students will be able to:

1. Express concepts such as syntax, semantics and typing rules in a formal way;

2. Evaluate expressions in lambda calculus according to the definition of the reduction relation;

3. Determine whether or not expressions in lambda calculus are typable in the simple type system;

4. Implement lambda calculus expressions in a functional language such as Haskell or ML, or the functional fragment of Python;

5. Execute pi calculus processes according to the definition of the reduction relation, and determine bisimulation relationships between processes;

6. Determine whether or not processes in pi calculus are typable in the simple type system;

7. Implement pi calculus processes in a simulation environment or in an appropriate fragment of the Go programming language;

8. Connect both the lambda calculus and the pi calculus to logic under Curry-Howard correspondences, which make the foundation for functional and concurrent programming.

Students must submit at least 75% by weight of the components (including examinations) of the course's summative assessment.