Document Open Access Logo

Fast, Verified Computation for Candle

Authors Oskar Abrahamsson , Magnus O. Myreen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.4.pdf
  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Oskar Abrahamsson
  • Chalmers University of Technology, Gothenburg, Sweden
Magnus O. Myreen
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Abrahamsson, Oskar: Swedish Foundation for Strategic Research.
  • Myreen, Magnus O.: Swedish Foundation for Strategic Research.

Acknowledgements

We want to thank Jeremy Avigad, John Harrison, Tobias Nipkow and Freek Wiedijk for feedback we received when the first author prepared this as a chapter for his PhD thesis [Oskar Abrahamsson, 2022]. We thank Thomas Sewell for showing us how to benchmark in-logic evaluation in Isabelle/HOL.

Cite As Get BibTex

Oskar Abrahamsson and Magnus O. Myreen. Fast, Verified Computation for Candle. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ITP.2023.4

Abstract

This paper describes how we have added an efficient function for computation to the kernel of the Candle interactive theorem prover. Candle is a CakeML port of HOL Light which we have, in prior work, proved sound w.r.t. the inference rules of the higher-order logic. This paper extends the original implementation and soundness proof with a new kernel function for fast computation. Experiments show that the new computation function is able to speed up certain evaluation proofs by several orders of magnitude.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • Prover soundness
  • Higher-order logic
  • Interactive theorem proving

Metrics

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

Supplementary Materials

References

  1. Oskar Abrahamsson. A Verified Theorem Prover for Higher-Order Logic. PhD thesis, Chalmers University of Technology, 2022. Google Scholar
  2. Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Proof-producing synthesis of CakeML from monadic HOL functions. Journal of Automated Reasoning (JAR), 2020. URL: https://rdcu.be/b4FrU.
  3. Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A verified implementation of HOL Light. In June Andronick and Leonardo de Moura, editors, Interactive Theorem Proving (ITP), volume 237 of LIPIcs, pages 3:1-3:17, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.3.
  4. Klaus Aehlig, Florian Haftmann, and Tobias Nipkow. A compiled implementation of normalisation by evaluation. J. Funct. Program., 22(1):9-30, 2012. URL: https://doi.org/10.1017/S0956796812000019.
  5. Bruno Barras. Programming and computing in HOL. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 1869 of Lecture Notes in Computer Science, pages 17-37. Springer, 2000. URL: https://doi.org/10.1007/3-540-44659-1_2.
  6. Pierre Crégut. An abstract machine for lambda-terms normalization. In Gilles Kahn, editor, Conference on LISP and Functional Programming (LFP), pages 333-340. ACM, 1990. URL: https://doi.org/10.1145/91556.91681.
  7. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, International Conference on Automated Deduction (CADE), volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  8. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Mitchell Wand and Simon L. Peyton Jones, editors, International Conference on Functional Programming (ICFP), pages 235-246. ACM, 2002. URL: https://doi.org/10.1145/581478.581501.
  9. Florian Haftmann. Code generation from specifications in higher-order logic. PhD thesis, Technical University Munich, 2009. Google Scholar
  10. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Functional and Logic Programming (FLOPS), volume 6009 of Lecture Notes in Computer Science, pages 103-117. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12251-4_9.
  11. John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of Lecture Notes in Computer Science, pages 60-66. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  12. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  13. 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 (TPHOLs), volume 5170 of LNCS. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  14. Alexey Solovyev. HOL Light’s computelib. Accessed 2022-06-11. URL: https://github.com/jrh13/hol-light/blob/master/compute.ml.
  15. The Coq Development Team. The Coq reference manual. Accessed 2022-06-11. URL: https://coq.inria.fr/distrib/current/refman/.
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