Formal methods
- Certified programming with dependent types
- A freely available draft of the book published by MIT Press introducing the Coq proof assistant. This is now recommended reading for the M.Phil Proof assistants course. A copy of the printed book is available in the West Hub library.
- Concrete semantics with Isabelle/HOL
- The full text of the book by T. Nipkow and G. Klein based on the concrete semantics document included with the Isabelle/HOL distribution.
- Software foundations series
- A series of books offering a broad introduction to the mathematical foundations of reliable software. The first two volumes Logical foundations and Programming language foundations are recommended reading for the M.Phil course on Proof assistants.