Proof Assistants

Course material

Introduction slides

Isabelle material

The Isabelle part of the lecture follows the book Concrete Semantics with Isabelle/HOL, up to and including the semantics of the IMP programming language.

• First part of the slides to guide us through the material
• Demo files (tar / zip) to interact with in Isabelle
• Exercises for the book "Concrete Semantics with Isabelle/HOL" are available on its website as a PDF and as theory templates.

Recordings

Lecture recordings are available on Moodle (although there currently seems to be an access control issue, which we hope to sort out soon).

Installation instructions

Installing Isabelle

The course will use Isabelle 2025-2. You can download it from its website, and there are detailed installation instructions available here for Linux, Windows, and macOS (including workarounds for potential issues with signatures/certificates or anti-virus programs). We recommend using the jEdit prover IDE, which comes bundled with Isabelle.

Installing Lean

Lean includes a version manager which installs the right version automatically. This page explains how to install it through VS Code. People who do not wish to use VS Code can install it manually, and use the Neovim Plugin lean.nvim.