Document Open Access Logo

Ornaments for Proof Reuse in Coq

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.26.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Talia Ringer
  • University of Washington, USA
Nathaniel Yazdani
  • University of Washington, USA
John Leo
  • Halfaya Research, USA
Dan Grossman
  • University of Washington, USA

Acknowledgements

We thank Jasper Hugunin, James Wilcox, Jason Gross, Pavel Panchekha, and Marisa Kirisame for ideas that helped inform tool design. We thank Thomas Williams, Josh Ko, Matthieu Sozeau, Cyril Cohen, Nicolas Tabareau, and Enrico Tassi for help navigating related work. We thank Emilio J. Gallego Arias, Gaëtan Gilbert, Pierre-Marie Pédrot, and Yves Bertot for help understanding Coq plugin APIs. We thank Shachar Itzhaky and Tej Chajed for ideas for future directions. We thank the UW and UCSD programming languages labs for feedback. This material is based upon work supported by the National Science Foundation Graduate Research Fellowship under Grant No. DGE-1256082. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

Cite As Get BibTex

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.26

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • ornaments
  • proof reuse
  • proof automation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Gilles Barthe and Olivier Pons. Type isomorphisms and proof reuse in dependent type theory. In International Conference on Foundations of Software Science and Computation Structures, pages 57-71. Springer, 2001. Google Scholar
  2. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free: Parametricity for dependent types. Journal of Functional Programming, 22:107-152, March 2012. URL: https://doi.org/10.1017/S0956796812000056.
  3. Pierre Boutillier. New tool to compute with inductive in Coq. Theses, Université Paris-Diderot - Paris VII, February 2014. URL: https://tel.archives-ouvertes.fr/tel-01054723.
  4. Joshua E. Caplan and Mehdi T. Harandi. A logical framework for software proof reuse. In ACM SIGSOFT Software Engineering Notes, volume 20, pages 106-113. ACM, 1995. Google Scholar
  5. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. arXiv preprint, 2016. URL: http://arxiv.org/abs/1611.02108.
  6. Cyril Cohen and Damien Rouhling. A refinement-based approach to large scale reflection for algebra. In JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. URL: https://hal.inria.fr/hal-01414881.
  7. coq-club. [Coq-Club] Dealing with equalities in dependent types. http://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00099.html, 2017. Accessed: 2019-03-25.
  8. coq-club. [Coq-Club] Trouble with dependent induction. http://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00079.html, 2017. Accessed: 2019-03-25.
  9. Pierre-Évariste Dagand. The essence of ornaments. Journal of Functional Programming, 27, 2017. Google Scholar
  10. Pierre-Evariste Dagand and Conor McBride. A Categorical Treatment of Ornaments. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 530-539, Washington, DC, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2013.60.
  11. Pierre-Evariste Dagand and Conor McBride. Transporting functions across ornaments. Journal of functional programming, 24(2-3):316-383, 2014. Google Scholar
  12. Benjamin Delaware, William Cook, and Don Batory. Product Lines of Theorems. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '11, pages 595-608, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2048066.2048113.
  13. Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. Meta-theory à La Carte. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 207-218, New York, NY, USA, 2013. ACM. URL: https://doi.org/10.1145/2429069.2429094.
  14. Larry Diehl, Denis Firsov, and Aaron Stump. Generic Zero-Cost Reuse for Dependent Types. CoRR, abs/1803.08150, 2018. URL: http://arxiv.org/abs/1803.08150.
  15. Amy Felty and Douglas Howe. Generalization and reuse of tactic proofs. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 1-15. Springer, 1994. Google Scholar
  16. Brian Huffman and Ondřej Kunčar. Lifting and Transfer: A modular design for quotients in Isabelle/HOL. In International Conference on Certified Programs and Proofs, pages 131-146. Springer, 2013. Google Scholar
  17. Inria. The Coq Standard Library. http://coq.inria.fr/distrib/current/stdlib. Accessed: 2019-03-15.
  18. Einar Broch Johnsen and Christoph Lüth. Theorem reuse by proof term transformation. In International Conference on Theorem Proving in Higher Order Logics, pages 152-167. Springer, 2004. Google Scholar
  19. Hsiang-Shang Ko and Jeremy Gibbons. Relational algebraic ornaments. In Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, pages 37-48. ACM, 2013. Google Scholar
  20. Hsiang-Shang Ko and Jeremy Gibbons. Programming with ornaments. Journal of Functional Programming, 27, 2016. Google Scholar
  21. Nicolas Magaud. Changing data representation within the Coq system. In International Conference on Theorem Proving in Higher Order Logics, pages 87-102. Springer, 2003. Google Scholar
  22. Nicolas Magaud and Yves Bertot. Changing data structures in type theory: A study of natural numbers. In International Workshop on Types for Proofs and Programs, pages 181-196. Springer, 2000. Google Scholar
  23. Conor McBride. Ornamental algebras, algebraic ornaments, 2011. URL: http://plv.mpi-sws.org/plerg/papers/mcbride-ornaments-2up.pdf.
  24. Trevor L. McDonell, Timothy A. K. Zakian, Matteo Cimini, and Ryan R. Newton. Ghostbuster: A Tool for Simplifying and Converting GADTs. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 338-350, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2951913.2951914.
  25. Anders Miltner, Kathleen Fisher, Benjamin C Pierce, David Walker, and Steve Zdancewic. Synthesizing bijective lenses. Proceedings of the ACM on Programming Languages, 2(POPL):1, 2017. Google Scholar
  26. Olivier Pons. Generalization in type theory based proof assistants. In International Workshop on Types for Proofs and Programs, pages 217-232. Springer, 2000. Google Scholar
  27. Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting proof automation to adapt proofs. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 115-129. ACM, 2018. Google Scholar
  28. Matthieu Sozeau. Equations: A Dependent Pattern-Matching Compiler. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, pages 419-434, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  29. Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. hs-to-coq. https://github.com/antalsz/hs-to-coq, 2018-2019. Accessed: 2019-03-12.
  30. Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. Equivalences for Free: Univalent Parametricity for Effective Transport. Proc. ACM Program. Lang., 2(ICFP):92:1-92:29, July 2018. URL: https://doi.org/10.1145/3236787.
  31. Amin Timany and Bart Jacobs. First Steps Towards Cumulative Inductive Types in CIC. In ICTAC, 2015. Google Scholar
  32. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  33. Thomas Williams and Didier Rémy. A Principled Approach to Ornamentation in ML. Proc. ACM Program. Lang., 2(POPL):21:1-21:30, December 2017. URL: https://doi.org/10.1145/3158109.
  34. Theo Zimmermann and Hugo Herbelin. Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant. arXiv preprint, 2015. URL: http://arxiv.org/abs/1505.05028.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact