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
• Second part of the slides about the semantics of the IMP programming language
• Demo files (tar / zip) to interact with in Isabelle
• Selected exercises for the first practical session: Practical1.thy, AExp.thy
• Solutions (tar / zip archive)
• Selected exercises for the second practical session: Practical2.thy with supporting theories (tar / zip archive)
• Solutions (tar / zip archive)
• Exercises for the book "Concrete Semantics with Isabelle/HOL" are available on its website as a PDF and as theory templates.

Installation instructions for the proof assistants

Installing Isabelle

You can download the current version of Isabelle 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.