License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.26
URN: urn:nbn:de:0030-drops-110816
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11081/
Go to the corresponding LIPIcs Volume Portal

Ringer, Talia ; Yazdani, Nathaniel ; Leo, John ; Grossman, Dan

Ornaments for Proof Reuse in Coq

pdf-format:
LIPIcs-ITP-2019-26.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{ringer_et_al:LIPIcs:2019:11081,
  author =	{Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman},
  title =	{{Ornaments for Proof Reuse in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{26:1--26:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11081},
  URN =		{urn:nbn:de:0030-drops-110816},
  doi =		{10.4230/LIPIcs.ITP.2019.26},
  annote =	{Keywords: ornaments, proof reuse, proof automation}
}

Keywords: ornaments, proof reuse, proof automation
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The Coq plugin, examples, and case study code for this paper can be found at http://github.com/uwplse/ornamental-search/tree/itp+equiv.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI