Extensible and Efficient Automation through Reflective Tactics
Gregory Malecha and Jesper Bengtson
Foundational proof assistants simultaneously offer both expressive logics and strong guarantees. The price they pay for this flexibility is often the need to build and check explicit proof objects which can be expensive. In this work we develop a collection of techniques for building reflective automation, where proofs are witnessed by verified decision procedures rather than verbose proof objects. Our techniques center around a verified domain specific language for proving, Rtac, written in Gallina, Coq's logic. The design of tactics makes it easy to combine them into higher-level automation that can be proved sound in a mostly automated way. Furthermore, unlike traditional uses of reflection, Rtac tactics are independent of the underlying problem domain, which allows them to be re-tasked to automate new problems with very little effort. We demonstrate the usability of Rtac through several case studies demonstrating orders of magnitude speedups for relatively little engineering work.
Citation (BibTex)
@inbook{malecha2016easy-and-efficient,
author="Malecha, Gregory and Bengtson, Jesper",
editor="Thiemann, Peter",
chapter="Extensible and Efficient Automation Through Reflective Tactics",
title="Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings",
year="2016",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="532--559",
isbn="978-3-662-49498-1",
doi="10.1007/978-3-662-49498-1_21",
url="http://dx.doi.org/10.1007/978-3-662-49498-1_21"
}