Extensible and Efficient Automation Through Reflective Tactics

Gregory Malecha, Jesper Bengtson

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelProgramming 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
Antal sider28
ForlagSpringer
Publikationsdato22 mar. 2016
Sider532-559
ISBN (Trykt)978-3-662-49497-4
ISBN (Elektronisk)978-3-662-49498-1
DOI
StatusUdgivet - 22 mar. 2016
BegivenhedEuropean Symposium on Programming - Eindhoven University of Technology, Eindhoven, Holland
Varighed: 2 apr. 20167 apr. 2016
Konferencens nummer: 25
http://www.etaps.org/index.php/2016/esop

Konference

KonferenceEuropean Symposium on Programming
Nummer25
LokationEindhoven University of Technology
Land/OmrådeHolland
ByEindhoven
Periode02/04/201607/04/2016
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind9632
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Extensible and Efficient Automation Through Reflective Tactics'. Sammen danner de et unikt fingeraftryk.

Citationsformater