MGS 2025 - Modular Proofs in Isabelle/HOL

This is the course page for the Midlands Graduate School (MGS) 2025 course on Modular Proofs in Isabelle/HOL. MGS will be hosted at the University of Sheffield from the 7th to 11th of April 2025. For more information on the school (including registration), see the official MGS website.

Course Summary

Proof assistants are a vital tool in formal verification, and formal libraries have seen significant growth in the last decade. With this growth comes a need to focus not just on verifying an end result, but also on the process of engineering a “good” formal proof – considering factors such as modularity, reusability, and generality.

This course will aim to be an introduction to formal verification in Isabelle/HOL, including selective exploration of more advanced techniques that encourage such modularity in formal proofs. Centrally, this includes the use of Isabelle’s module system (locales) which offer several advantages, including building modular hierarchies and transferring results between different object representations. The course will also aim to introduce other related constructs in Isabelle (e.g. typeclasses).

Formalisation examples will draw on both concepts from mathematics (e.g. algebra/combinatorics) and programming language semantics – the necessary background will be provided in both cases. No previous experience in using proof assistants is required.

Course Resources

All students should pre-install Isabelle/HOL - see the Isabelle website.

Course resources will become available closer to the date.