Extensible and Efficient Automation Through Reflective Tactics

Gregory Malecha, Jesper Bengtson

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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. This 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.
Original languageEnglish
Title of host publicationProgramming 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
Number of pages28
Publication date22 Mar 2016
ISBN (Print)978-3-662-49497-4
ISBN (Electronic)978-3-662-49498-1
Publication statusPublished - 22 Mar 2016
EventEuropean Symposium on Programming - Eindhoven University of Technology, Eindhoven, Netherlands
Duration: 2 Apr 20167 Apr 2016
Conference number: 25


ConferenceEuropean Symposium on Programming
LocationEindhoven University of Technology
Internet address
SeriesLecture Notes in Computer Science


  • Proof by reflection
  • Coq
  • Interactive proof assistants


Dive into the research topics of 'Extensible and Efficient Automation Through Reflective Tactics'. Together they form a unique fingerprint.

Cite this