MGS 2025 - Modular Proofs in Isabelle/HOL
MGS 2025 Course Page
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). We’ll move quickly from going through Isabelle basics (lecture 1) to exploring advanced formalisation examples in lecture 3 and 4.
Formalisation examples will draw on both concepts from mathematics (e.g. algebra/combinatorics) and programming language semantics – a brief summary of the necessary background will be provided in both cases. No previous experience in using proof assistants is required.
Lecture Plan
The lectures plan to cover the following topics
- Lecture 1: Motivation and history of formalisation, overview of proof assistant landscape and an introduction to Isabelle basics (foundations, propositional logic, functions, datatypes, induction etc).
- Lecture 2: Introducing modularity. Finish off Isabelle “tour” with Isar and more types, introduce type classes and locale basics with examples.
- Lecture 3: Formalisation of mathematics (combinatorics). Some history/recent developments, motivating a combinatorial case study plus a brief overview of mathematical background, using locales to create large hierarchies, locale reasoning patterns, locales in proofs.
- Lecture 4: Modular “program” verification: working with semantics in Isabelle/HOL (+ inductive definitions), using locales for abstraction and refinement, using locales to model interesting properties (with current research examples).
The schedule is available on the MGS website. This course has four afternoon lectures and four morning exercise sessions.
Course Resources
All students should pre-install Isabelle/HOL - see the Isabelle website.
The course materials (draft) are available below. Lecture slides offer a two per page and single option. Please check for updates throughout the week. Feedback very welcome!
| Day | Lecture Notes | Lecture Notes (2 page) | Isabelle Theories |
|---|---|---|---|
| Monday | Lecture 1 | Lecture 1 x2 | Isabelle 1 Zip |
| Tuesday | Lecture 2 | Lecture 2 x2 | Isabelle 2 Zip |
| Wednesday | Lecture 3 | Lecture 3 x2 | Isabelle 3 Zip |
| Thursday | Lecture 4 | Lecture 4 x2 | Isabelle 4 Zip |
Material for the exercise sessions is below (check for updates throughout the week):
| Day | Isabelle Theories | Solutions |
|---|---|---|
| Tuesday | Ex1 Theory | |
| Wednesday | Ex2 Theory | |
| Thursday | Ex3 Theories | |
| Friday | Ex4 Theory |
Other Useful Resources
For more information on Isabelle/detail on different features, see:
- The Isabelle distribution comes with extensive documentation. In particular the prog-prove and locales/type classes tutorials may prove useful.
- For program verification, consider Nipkow and Klein’s Concrete Semantics book
- For history, interesting notes, and more detailed examples, the Machine Logic blog by Larry Paulson may prove interesting.