An Isabelle Proof Method Language

Select |




Print


Matichuk, Daniel; Wenzel, Makarius; Murray, Toby

Matichuk, Daniel; Wenzel, Makarius; Murray, Toby


2014-07-14


Conference Material


Interactive Theorem Proving (ITP)


Vienna, Austria


390-405


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.


Springer


proof automation, proof procedure language, Isabelle


https://doi.org/10.1007/978-3-319-08970-6_25


http://www.cs.uwyo.edu/~ruben/itp-2014/Main/Home


nicta:7847


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. https://doi.org/10.1007/978-3-319-08970-6_25



Loading citation data...

Citation counts
(Requires subscription to view)