Document Open Access Logo

A Verified Cyclicity Checker: For Theories with Overloaded Constants

Authors Arve Gengelbach , Johannes Åman Pohjola

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.15.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Arve Gengelbach
  • KTH Royal Institute of Technology, Stockholm, Sweden
Johannes Åman Pohjola
  • University of New South Wales, Sydney, Australia

Acknowledgements

We are grateful to Andrei Popescu and Tjark Weber for technical discussion. We thank the anonymous reviewers for their constructive feedback. This work was begun while the first author was affiliated with Uppsala University, Sweden.

Cite AsGet BibTex

Arve Gengelbach and Johannes Åman Pohjola. A Verified Cyclicity Checker: For Theories with Overloaded Constants. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.15

Abstract

Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Correctness
  • Theory of computation → Program verification
  • Theory of computation → Higher order logic
  • Theory of computation → Graph algorithms analysis
Keywords
  • cyclicity
  • non-termination
  • ad-hoc overloading
  • definitions
  • Isabelle/HOL

Metrics

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

Related Versions

Supplementary Materials

References

  1. Johannes Åman Pohjola and Arve Gengelbach. A Mechanised Semantics for HOL with Ad-hoc Overloading. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 498-515. EasyChair, 2020. URL: https://doi.org/10.29007/413d.
  2. Rob Arthan. HOL constant definition done right. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 531-536. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_34.
  3. Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauß, and Klaus U. Schulz. Unification Theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/b978-044450813-3/50010-2.
  4. Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, and Robert E. Tarjan. A New Approach to Incremental Cycle Detection and Related Problems. ACM Trans. Algorithms, 12(2):14:1-14:22, 2016. URL: https://doi.org/10.1145/2756553.
  5. Jared Curran Davis. A self-verifying theorem prover. The University of Texas at Austin, 2009. Google Scholar
  6. Maxime Dénès. [Coq-Club] Propositional extensionality is inconsistent in Coq, December 2013. Coq Club Mailinglist. URL: https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html.
  7. Arve Gengelbach and Johannes Åman Pohjola. Towards Correctly Checking for Cycles in Overloaded Definitions. Technical Report 2021-001, Department of Information Technology, Uppsala University, March 2021. URL: http://www.it.uu.se/research/publications/reports/2021-001/.
  8. Arve Gengelbach, Johannes Åman Pohjola, and Tjark Weber. Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. In Claudio Sacerdoti Coen and Alwen Tiu, editors, Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020, volume 332 of EPTCS, pages 1-17, 2020. URL: https://doi.org/10.4204/EPTCS.332.1.
  9. Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.18.
  10. John Harrison. Towards self-verification of HOL light. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 177-191. Springer, 2006. URL: https://doi.org/10.1007/11814771_17.
  11. Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, and Michael Norrish. Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 646-662. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_42.
  12. Jacques-Henri Jourdan. Coq pull request #90, July 2015. URL: https://github.com/coq/coq/pull/89.
  13. Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. J. Autom. Reason., 56(3):221-259, 2016. URL: https://doi.org/10.1007/s10817-015-9357-x.
  14. Ondřej Kunčar. Correctness of Isabelle’s Cyclicity Checker: Implementability of Overloading in Proof Assistants. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 85-94. ACM, 2015. URL: https://doi.org/10.1145/2676724.2693175.
  15. Ondřej Kunčar and Andrei Popescu. A Consistent Foundation for Isabelle/HOL. J. Autom. Reason., 62(4):531-555, 2019. URL: https://doi.org/10.1007/s10817-018-9454-8.
  16. Tobias Nipkow. What’s in Main, December 2021. URL: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/main.pdf.
  17. Tobias Nipkow and Simon Roßkopf. Isabelle’s Metalogic: Formalization and Proof Checker. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 93-110. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_6.
  18. Steven Obua. Checking Conservativity of Overloaded Definitions in Higher-Order Logic. In Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, pages 212-226. Springer, 2006. URL: https://doi.org/10.1007/11805618_16.
  19. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  20. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang., 4(POPL):8:1-8:28, 2020. URL: https://doi.org/10.1145/3371076.
  21. Matthieu Sozeau and Nicolas Oury. First-class type classes. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 278-293. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  22. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 499-514. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_32.
  23. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. J. Funct. Program., 29:e2, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  24. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 60-76. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75283.
  25. Makarius Wenzel. The Isabelle/Isar Reference Manual, December 2021. URL: https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/isar-ref.pdf.
  26. Markus Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy P. Felty, editors, Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, volume 1275 of Lecture Notes in Computer Science, pages 307-322. Springer, 1997. URL: https://doi.org/10.1007/BFb0028402.
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 Imprint Privacy Contact