Course pages 2017–18

Interactive Formal Verification

Course texts

The primary course text is "Concrete Semantics" by T. Nipkow and G. Klein, and is freely available here. A stripped-down version of this book is supplied with the Isabelle distribution (click the "Documentation" button on the right, and then open "prog-prove" under the "Tutorials" heading), and is called "Programming and proving with Isabelle/HOL". Some material is common to both, but numbered differently. I will reference both.

The additional technical manuals also found under the "Tutorials" heading in the Isabelle documentation panel are also suggested reading for anybody who wishes to advance their usage of Isabelle. The older (but still relevant) Isabelle tutorial, found in the "Documentation" panel under the "Old tutorials" heading also handles some subjects in more detail than "Programming and proving with Isabelle/HOL".

Students are also encouraged to read through existing Isabelle formalisations to learn idioms and tricks from experienced Isabelle users. A good source of vetted Isabelle formalisations, covering a range of subjects in pure mathematics and computer science, is the Archive of Formal Proofs.

Installing Isabelle

Isabelle should be installed on laboratory machines. However, if you wish to install Isabelle on your own machine, then (assuming a Linux install):

1. Download the Isabelle2016-1 distribution from the Isabelle homepage (click here). Move the tar file into a suitable location, and then execute tar xzf Isabelle2016-1_app.tar.gz to unpack. Add the resulting Isabelle2016-1/bin/ directory to your PATH (usually by editing .bashrc or some other similar file in your home directory).
2. Start Isabelle for the first time by executing Isabelle2016-1 from a terminal window. This will first build a PolyML heap for the HOL object logic which can take up to 15 minutes depending on the speed of your machine. This heap building will only happen on the first execution of Isabelle. One this process has finished, close the dialogue box and proceed to edit your theory files.

Distributions for Windows and MacOS are also available from the Isabelle homepage.

Lectures

All lectures will be interactive and held in the computer labs. Each lecture has an associated Isabelle theory file, with the intention that students are sat at machines inspecting the contents of the file within Isabelle itself whilst I project the contents of my own screen, explaining what is going on. The ordering of, and time spent on, any one particular topic is therefore subject to change based on how well we progress.

Each lecture (other than the first, introductory lecture) also has a set of associated exercises which students are encouraged to complete during the lab sessions, as the course progresses. Lectures are only intended to push students in the right direction, and provide a decent footing for further learning. Mastering Isabelle will require considerable practice and hard work. Students are encouraged to do further reading and think up their own exercises in their own time.

Lab-based practical sessions

Lab sessions will be held on 12th October, 19th October, 2nd November and 9th November. All lab sessions will be held in SW02 at 11am (i.e. immediately after that morning's lecture). Sessions will be supervised by Dr. Victor Gomes and Dr. Dominic Mulligan (for the first two), and are intended for students to practice Isabelle/HOL skills and ask questions.

Errata

With thanks for Bradley Hardy, Sebastian Borgeaud-dit-Avocat, and Patrick Fernandes:

The exercise sheet for recursive functions and datatypes contained a mistaken in the definition of a rose tree. The sheet has been amended to remove the broken material.

The definition of continuity in the second assessment was changed.

Other interactive proof assistants

Several other interactive theorem proving systems exist, and are in active use. Ideas are often shared between these systems, and it is often worth looking at work published using these systems for new ideas. The major conferences in the field are CADE, CAV, CPP, and ITP, where work carried out in all of the theorem provers below is presented.