This course will introduce the use of interactive proof assistants both for mathematics and for work in software verification. We will introduce the basics of interactive theorem proving using the proof assistant Isabelle/HOL. Starting from elementary logical formulae, we will prove many theorems “live” in lectures, and apply what we have learned to proof exercises and challenges. Proof assistants can be both very fun and very addictive in equal measure. It is my hope to share that fun with you.

1. Propositional and first-order logic, natural deduction proofs. Types, definitions, unfolding.
2. Simplifier, rewriting, function definitions, other definitions.
3. Structural induction, inductive definitions, induction tactics.
4. Structured proofs in Isar, calculational proofs.
5. More automatic methods, sledgehammer.

Remaining topics to be covered if there is time:

• General recursion and termination measures
• Type classes and locales
• Program verification with SIMPL or AutoCorres
• Designing tactics with Eisbach

Some familiarity with simple first order and propositional logic is assumed. Some functional programming experience (in particular, some familiarity with lambda calculus or a language like Haskell) is also recommended.

Concrete Semantics, Tobias Nipkow and Gerwin Klein

Liam O'Connor is a Senior Lecturer at the Australian National University and an Honorary Fellow at the University of Edinburgh, where he worked until 2024. He obtained his PhD from UNSW in 2019, the dissertation for which received the John Makepeace Bennett award. He has broad interests in theoretical computer science, especially in semantics, models and specifications, as well as in the application of these theoretical techniques to practical problems in programming languages, systems and software engineering.