The University of New South Wales

Eisbach: High Level Proof Methods for Isabelle

The Eisbach project has successfully concluded with Daniel Matichuk's PhD thesis (see below in publications). The Eisbach proof method language is now available in the Isabelle distribution.

Below is an archive of the original project goals and web page.


Abstract PDF Daniel Matichuk
Automation for proof engineering: Machine-checked proofs at scale
PhD Thesis, UNSW, Sydney, Australia, 2018
Abstract PDF Yutaka Nagashima
Keep failed proof attempts in memory
Isabelle Workshop 2016, Nancy, France, August, 2016
Abstract PDF Daniel Matichuk, Toby Murray and Makarius Wenzel
Eisbach: A proof method language for isabelle
Journal of Automated Reasoning, Volume 56, Number 3, pp. 261–282, March, 2016
Abstract PDF Daniel Matichuk, Makarius Wenzel and Toby Murray
An Isabelle proof method language
International Conference on Interactive Theorem Proving, pp. 390–405, Vienna, Austria, July, 2014