@inproceedings{ringer-2019-ornaments,
  doi = {10.4230/LIPICS.ITP.2019.26},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.26},
  author = {Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan},
  keywords = {ornaments, proof reuse, proof automation, Software and its engineering → Formal software verification},
  language = {en},
  title = {Ornaments for Proof Reuse in Coq},
  volume = {141},
  pages = {26:1-26:19},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2019},
  copyright = {Creative Commons Attribution 3.0 Unported license},
  booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}
}