An Isabelle Proof Method Language

Select |


Matichuk, Daniel; Wenzel, Makarius; Murray, Toby

Matichuk, Daniel; Wenzel, Makarius; Murray, Toby


Conference Material

Interactive Theorem Proving (ITP)

Vienna, Austria


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 more duplication in large proofs than is desirable. In this paper we present a proof method language for Isabelle, which aims to fill this gap by incorporating Isar language elements, thus making it accessible to existing users. We describe the language and the design principles on which it was developed. We evaluate its effectiveness by implementing some tactics widely-used in the seL4 verification stack, and report on its strengths and limitations.


proof automation, proof procedure language, Isabelle


Matichuk, Daniel; Wenzel, Makarius; Murray, Toby. An Isabelle Proof Method Language. In: Gerwin Klein and Ruben Gamboa Editor, editor/s. Interactive Theorem Proving (ITP); Vienna, Austria. Springer; 2014-07-14. 390-405.

Loading citation data...

Citation counts
(Requires subscription to view)