License
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://drops.dagstuhl.de/opus/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
Seminar: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 06.09.2019


DROPS-Home | Imprint | Privacy Published by LZI