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)
- McCarthy's original Lisp paper
- Landin's The next 700 programming languages (ISWIM)
- Gordon et al. A Metalanguage for interactive proof in LCF (ML)
- Turner's Miranda: A non-strict functional language with polymorphic types
- Hudak The Conception, Evolution, and Application of Functional Programming Languages
- Hudak et al. A History of Haskell: being lazy with class
Lecture 2: Formal specification and big-step operational semantics (slides)
- A gentle introduction to HOL: A Machine-Oriented Formulation of Higher-Order Logic by Gordon
- Proof assistants: HOL4, HOL Light and Isabelle/HOL (Paulson's MPhil course on Isabelle/HOL)
- Plotkin: A Structural Approach to Operational Semantics
- Plotkin: The Origins of Structural Operational Semantics
- Kahn: Natural semantics
Lecture 3: Small-step operational semantics and SML (slides)
- Danvy: A Rational Deconstruction of Landin's SECD Machine
- Felleisen and Friedman introduce the CEK-machine: Control Operators, the SECD-Machine, and the Lambda-Calculus
- Krivine: A call-by-name lambda-calculus machine
- Harper, Milner and Tofte define SML: The Definition of Standard ML – Version 2
- Tools that aid writing formal semantics: Lem and Ott
- Owens: A formal semantics (both small-step and big-step) for a significant subset of SML
Lecture 4: Machine code, formal verification and decompilation (slides)
- Instruction set architecture documentation: Intel x86, AMD x86, ARM; Power; MIPS.
- Tutorials on x64 assembly programming: 64-bit x86 with NASM and Linux, 64-bit x86 with Visual Studio, 32-bit x86.
- Hoare: Retrospective: An Axiomatic Basis for Computer Programming
- First 'real' formal verification of machine code: Boyer and Yu's paper from 1996
- Myreen: Decompilation into logic and decompilation of an OS micro-kernel
- Reynolds: Separation logic
Lecture 5: Memory abstraction, verification of a garbage collector (slides)
- Padron-McCarthy's The Very Basics of Garbage Collection
- Wikipedia's entry on garbage collection explains terminology.
- McCreight et al. A general framework for certifying garbage collectors and their mutators
- Gonthier's Verifying the safety of a practical concurrent garbage collector
Lecture 6: Memory abstraction formalised, construction of verified interpreter (slides)
- Exaplanation of memory representation: Why is an int in OCaml only 31 bits?
- 31-bit integers: Efficient Arithmetic on Small Integers
- Chapters 6 and 7 of Myreen's PhD thesis: Formal verification of machine-code programs
Lecture 7: Verified compilation of a first-order Lisp language (slides — corrected on 3 Nov 2013)
- Leroy: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant
- Sevcik et al. Relaxed-Memory Concurrency and Verified Compilation
- Myreen's compiler for first-order-ish Lisp: A verified runtime for a verified theorem prover
- Lambda lifting
- Kennedy: Compiling with Continuations, Continued
- Chlipala: A Verified Compiler for an Impure Functional Language
- Peyton Jones: Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-machine
- Nanopass Compiler Framework
- Milner: A theory of type polymorphism in programming
- Wright and Felleisen: A Syntactic Approach to Type Soundness
- Leroy: Manifest types, modules, and separate compilation
- Owens: A sound semantics for OCaml light
- Löh et al. A tutorial implementation of a dependently typed lambda calculus
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)
- Koprowski and Binsztok on mechanised PEGs
- Ford on PEGs: Parsing expression grammars: a recognition-based syntactic foundation
- Soundness and completeness of PEG for ML: Kumar et al. CakeML: a verified implementation of ML
- Barthwal and Norrish on verified SLR parsing
- Jourdan, Pottier and Leroy on automaton verification (“verifying yacc”)
Lecture 13: Semantic preservation for non-terminating programs (slides)
- Clocked big-step semantics for ML: Kumar et al. CakeML: a verified implementation of ML
- Milner and Tofte: Co-induction in Relational Semantics
- Frost: A Case Study of Co-induction in Isabelle HOL
- Leroy and Grall: Coinductive big-step operational semantics
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.
- Madhavapeddy et al. Unikernels: Library Operating Systems for the Cloud