Ornaments for proof reuse in Coq

Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publication10th International Conference on Interactive Theorem Proving, ITP 2019
EditorsJohn Harrison, John O'Leary, Andrew Tolmach
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959771221
StatePublished - Sep 2019
Externally publishedYes
Event10th International Conference on Interactive Theorem Proving, ITP 2019 - Portland, United States
Duration: Sep 9 2019Sep 12 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


Conference10th International Conference on Interactive Theorem Proving, ITP 2019
Country/TerritoryUnited States


  • Ornaments
  • Proof automation
  • Proof reuse

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Ornaments for proof reuse in Coq'. Together they form a unique fingerprint.

Cite this