Ornaments for Proof Reuse in Coq

Talia Ringer, Nathaniel Yazdani, John Leo & Dan Grossman
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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.