Sciweavers

JAR
2016

Eisbach: A Proof Method Language for Isabelle

7 years 11 months ago
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.
Daniel Matichuk, Toby C. Murray, Makarius Wenzel
Added 06 Apr 2016
Updated 06 Apr 2016
Type Journal
Year 2016
Where JAR
Authors Daniel Matichuk, Toby C. Murray, Makarius Wenzel
Comments (0)