Tutorial on The Isabelle Refinement Framework and Autoref

About the Refinement Framework

The Isabelle Refinement and Autoref Frameworks support a stepwise refinement approach to verified program development, using the theorem prover Isabelle/HOL. It can be used to produce verified, efficiently executable algorithms. It is accompanied by the Isabelle Collection Framework, which provides an extensive library of reusable verified functional data structures.

Here are some examples for algorithms and software systems that use the Refinement Framework:

While this tutorial covers refinement to purely functional programs only, the Sepref-Tool also supports refinement to imperative programs. The above link also contains a userguide, which may be a good follow-up to this tutorial / an alternative to the Autoref-part of this tutorial.

About this Tutorial

This tutorial covers the basics of the refinement framework and the Autoref tool. It is a combination of some theoretical background, tool demo, and do-it-yourself parts. It can be given in roughly two days.

It requires a solid knowledge of Isabelle, and a bit of background in Hoare logic and programming with monads.

Material

Note:The theories require Isabelle 2016 with the AFP component installed.
refine_tutorial.tgz
run isabelle.sh to start the IDE. On first invocation, it will build the image, which will take some time.
Slides: refine_slides.pdf
Old Isabelle 2014 version: refine_tutorial.tgz