Providing documentation and testcases for the theorem prover Isabelle
Final Report Abstract
This project was about helping the development of the Isabelle theorem prover. This theorem prover is part of the research infrastructure for a sizeable academic community concerned with formalising mathematics and proving the correctness of computer programs. Like every software, this theorem prover depends on capable developers that need to be trained for working with the existing code base. In this project we have generated an electronic textbook that helps with understanding the mathematical concepts behind the Isabelle theorem prover and the plethora of programming “tricks” that have been accumulated over the years in the code base of this theorem prover. We have received help from 11 authors and received feedback about the usefulness of the material we provided. We believe this project has thus helped the continued maintenance of the Isabelle theorem prover and has educated a new generation of developers.
Publications
- The Isabelle Programming Cookbook
Christian Urban, Stefan Berghofer, Jasmin Blanche e, Sascha Böhme, Lukas Bulwahn, Jeremy Dawson, Rafal Kolanski, Alexander Krauss, Tobias Nipkow, Andreas Schropp, Christian Sternagel
