Computer Laboratory

Course pages 2013–14

Functional Programming: Implementation, Specification and Verification

Tick exercises: see assessment page.

What is examinable? Answer: everything that is lectured is examinable, except the supplementary material and Lecture 16.

Lecture 1: Introduction, history of FP and core concepts (slides)

Supplementary material:

Lecture 2: Formal specification and big-step operational semantics (slides)

Supplementary material:

Lecture 3: Small-step operational semantics and SML (slides)

Supplementary material:

Lecture 4: Machine code, formal verification and decompilation (slides)

Supplementary material:

Lecture 5: Memory abstraction, verification of a garbage collector (slides)

Supplementary material:

Lecture 6: Memory abstraction formalised, construction of verified interpreter (slides)

Supplementary material:

Lecture 7: Verified compilation of a first-order Lisp language (slides — corrected on 3 Nov 2013)

Supplementary material:

Lecture 8: Verified compilation of closures — guest lecture by Ramana Kumar (slides, slides as PDF)

Supplementary material:

Lecture 9: Types, type soundness and verified type inference — guest lecture by Scott Owens (slides — extended with two new slides on 13 Nov 2013)

Supplementary material:

Lecture 10: Verified compilation of closures, continued — guest lecture by Ramana Kumar (same slides as Lecture 8)

Lecture 11: Verified compilation of closures, continued — guest lecture by Ramana Kumar (same slides as Lecture 8)

Lecture 12: Verified Parsing — guest lecture by Michael Norrish (slides)

Supplementary material:

Lecture 13: Semantic preservation for non-terminating programs (slides)

Supplementary material:

Lecture 14: A typed foreign function interface for ML — guest lecture by Jeremy Yallop (slide set 1, slide set 2)

Lecture 15: Abstractions for programming in the large: the ML module system — guest lecture by Jeremy Yallop (slides)

Lecture 16: Using ML at scale: building a modular operating system — guest lecture by Anil Madhavapeddy (slides)

Abstract:

One of the main attractions of ML implementations, and OCaml in partcular, is its extremely powerful module system. Large code bases can be factored into thousands of reusable modules that can be parameterised across other modules. This makes the maintenance of multi-million line codebases a bearable task, and indeed OCaml's dominant use in industry is found in large, mission-critical codebases.

In this lecture, I'll walk you through a clean-slate operating system we've been building in the Computer Lab called MirageOS. It is written entirely in OCaml, and consists of a set of reusable modules which implements a complete set of OS functionality.

We'll start with building a simple website in UNIX, and then progressively add more modules to remove UNIX functionality and make the operating system self-hosting. Through this process, you'll see how the static type system in ML provides many abstractions "for free" at compilation time, providing a powerful balance between flexibilty and safety for building systems code.

Supplementary material: