LIPIcs.ITP.2019.26.pdf
- Filesize: 0.49 MB
- 19 pages
Document
Ornaments for Proof Reuse in Coq
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Acknowledgements
We thank Jasper Hugunin, James Wilcox, Jason Gross, Pavel Panchekha, and Marisa Kirisame for ideas that helped inform tool design. We thank Thomas Williams, Josh Ko, Matthieu Sozeau, Cyril Cohen, Nicolas Tabareau, and Enrico Tassi for help navigating related work. We thank Emilio J. Gallego Arias, Gaëtan Gilbert, Pierre-Marie Pédrot, and Yves Bertot for help understanding Coq plugin APIs. We thank Shachar Itzhaky and Tej Chajed for ideas for future directions. We thank the UW and UCSD programming languages labs for feedback. This material is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-1256082. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.
Cite AsGet BibTex
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.26
https://doi.org/10.4230/LIPIcs.ITP.2019.26
Abstract
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
Subject Classification
ACM Subject Classification
- Software and its engineering → Formal software verification
Keywords
- ornaments
- proof reuse
- proof automation
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads