Isabelle/HOL tutorial/documentation needed [closed]

Question

Closed. This question does not meet Stack Overflow guidelines. It is not currently accepting answers.

---

We don’t allow questions seeking recommendations for books, tools, software libraries, and more. You can edit the question so it can be answered with facts and citations.

Closed 5 years ago.

Improve this question

I am looking for freely available and good quality tutorials and documentation for Isabelle2013/HOL (aside of the obvious ones after Google-ing and digging a bit). Could you please recommend some?

Answer 1

Some documents that may help get you started:

• The previous de-facto tutorial was A Proof Assistant for Higher-Order Logic by Nipkow, Paulson and Wenzel. This document provides an introduction to Isabelle/HOL as a functional programming language as well as a guide as to how to use most of the common proof mechanisms available in Isabelle/HOL. It is a good starting point;

• A newer tutorial is Programming and Proving in Isabelle/HOL by Nipkow. It covers some of the same material as the previous document and is not quite as in-depth, but uses more modern techniques of carrying out proofs in Isabelle/HOL. It may be useful as a "quick-start" to Isabelle/HOL.

• The freely available book Concrete Semantics by Nipkow and Klein provides an introduction to Isabelle/HOL in the context of performing proofs on programming languages. If your interest in Isabelle/HOL is to do with program verification, this book would be a good start.

Is general, most (but not all) good reference guides are linked to from the Isabelle documentation page itself. watch out, however, as some of the documents there are quite old and unlikely to be relevant any longer, (though such documents have been tagged as such).

There are also a plethora of slides and lecture notes available of the web, such as UNSW or the University of Edinburgh, but these are probably better used as a supplement, as they often lack context and important details which are provided in the lectures.