Computer Laboratory

Course pages 2013–14

Functional Programming: Implementation, Specification and Verification

Principal lecturers: Prof Mike Gordon, Dr Magnus Myreen
Taken by: MPhil ACS, Part III
Code: L26
Hours: 16


This course has two aims that will be addressed in parallel. The first aim is to teach basics of functional programming languages and how they are implemented. The second aim is to teach how such concepts can be modelled precisely, using formal specifications, and how proof can be used to establish, to a high degree of assurance, that their low-level implementations faithfully implement the high-level specifications.


  • Functional programming: basic terminology, core concepts, its history
  • Specification: operational semantics, inductively defined relations
  • Target: machine code, memory management, garbage collection
  • Implementations: basic interpreter, static/dynamic compilation
  • Closures: compilation and formal reasoning
  • Types: what types bring in terms of safety and optimisations
  • Essential Optimisations: tail-call optimisation, etc.
  • Parallel programming and real-world use


On completion of this module students should:

  • understand what functional programming is, what different variants there are and have some grasp of their history;
  • explain the semantics of different functional languages using precise formal specifications;
  • know how to implement functional languages and what optimisations are important;
  • be able to state and critique what it means for an implementation of a functional programming language to be correct;
  • be able to (in principle) formally prove correctness of their implementations, including their compilers and garbage collectors;


  • Two ticked exercises during the course (20% of the final mark) and
  • a take-home test at the end of the course (80%).

Recommended reading

None listed yet.