ITU

Extensible and Efficient Automation Through Reflective Tactics

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

View graph of relations

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
PublisherSpringer
Publication date22 Mar 2016
Pages532-559
ISBN (Print)978-3-662-49497-4
ISBN (Electronic)978-3-662-49498-1
DOIs
Publication statusPublished - 22 Mar 2016
EventEuropean Symposium on Programming - Eindhoven University of Technology, Eindhoven, Netherlands
Duration: 2 Apr 20167 Apr 2016
Conference number: 25
http://www.etaps.org/index.php/2016/esop

Conference

ConferenceEuropean Symposium on Programming
Nummer25
LocationEindhoven University of Technology
LandNetherlands
ByEindhoven
Periode02/04/201607/04/2016
Internetadresse
SeriesLecture Notes in Computer Science
Volume9632
ISSN0302-9743
Close

    Research areas

  • Proof by reflection, Coq, Interactive proof assistants

Downloads

No data available

ID: 81631206