Eisbach: A Proof Method Language for Isabelle

Abstract Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance challenge. Isabelle’s most popular language interface, Isar, is attractive for new users, and powerful in the hands of experts, but has previously lacked a means to write automated proof procedures. This can lead to undesirable duplication in large proofs. In this paper we present Eisbach, a proof method language for Isabelle, which aims to fill this gap by incorporating Isar language elements, thus making it accessible to end-users. We describe the language and the design principles on which it was developed. We evaluate its effectiveness by implementing some proof tools that are widely-used in the seL4 verification stack, and report on its strengths and limitations.

• Type: Journal
• Year: 2016
• Where: JAR
• Authors: Daniel Matichuk, Toby C. Murray, Makarius Wenzel
• Keywords: Algorithms, JAR 2016