Document Open Access Logo

The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)

Author Magnus O. Myreen

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.1.pdf
  • Filesize: 0.51 MB
  • 10 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
Keywords
  • Program verification
  • interactive theorem proving

Metrics

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

Abstract

The CakeML project has developed a proof-producing code generation mechanism for the HOL4 theorem prover, a verified compiler for ML and, using these, a number of verified application programs that are proved correct down to the machine code that runs them (in some cases, even down to the underlying hardware). The purpose of this extended abstract is to tell the story of the project and to point curious readers to publications where they can read more about specific contributions.

Cite As Get BibTex

Magnus O. Myreen. The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.1

Author Details

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

Funding

This work was partially supported by the Swedish Foundation for Strategic Research, and by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.

Acknowledgements

I thank the ITP programme committee for inviting me to give this talk. I am grateful for comments on drafts of this text from Michael Norrish, Johannes Åman Pohjola, Andreas Lööw, Yong Kiam Tan, Oskar Abrahamsson and Konrad Slind. I want to thank the team of CakeML contributors for making the CakeML project such a pleasure to work on. Finally, I would like to thank the late Mike Gordon whose enthusiasm for the CakeML project and belief in its contributions are still felt and appreciated to this day.

Supplementary Materials

References

  1. Oskar Abrahamsson. A verified proof checker for higher-order logic. Journal of Logical and Algebraic Methods in Programming, 112:100530, 2020. URL: https://doi.org/10.1016/j.jlamp.2020.100530.
  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. Google Scholar
  3. Oskar Abrahamsson and Magnus O. Myreen. Automatically introducing tail recursion in CakeML. In Meng Wang and Scott Owens, editors, Trends in Functional Programming (TFP), volume 10788 of LNCS, pages 118-134. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-89719-6_7.
  4. Johannes Aman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic formulae for liveness properties of non-terminating CakeML programs. In Interactive Theorem Proving (ITP). LIPICS, 2019. Google Scholar
  5. Heiko Becker, Eva Darulova, Magnus O. Myreen, and Zachary Tatlock. Icing: Supporting fast-math style optimizations in a verified compiler. In Computer Aided Verification (CAV). Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_10.
  6. Heiko Becker, Nikita Zyuzin, Raphael Monat, Eva Darulova, Magnus O. Myreen, and Anthony Fox. A verified certificate checker for finite-precision error bounds in Coq and HOL4. In Formal Methods in Computer Aided Design (FMCAD). IEEE, 2018. Google Scholar
  7. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. VeriPhy: verified controller executables from verified cyber-physical system models. In Jeffrey S. Foster and Dan Grossman, editors, Programming Language Design and Implementation (PLDI), pages 617-630. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192406.
  8. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In International Conference on Functional Programming (ICFP). ACM, 2011. URL: https://doi.org/10.1145/2034773.2034828.
  9. Adam Sandberg Ericsson, Magnus O. Myreen, and Johannes Åman Pohjola. A verified generational garbage collector for CakeML. Journal of Automated Reasoning (JAR), 63, 2019. URL: https://doi.org/10.1007/s10817-018-9487-z.
  10. Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. Program verification in the presence of I/O - semantics, verified library routines, and verified applications. In Verified Software: Theories, Tools, Experiments (VSTTE), 2018. URL: https://doi.org/10.1007/978-3-030-03592-1_6.
  11. Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar. Verified compilation of CakeML to multiple machine-code targets. In Yves Bertot and Viktor Vafeiadis, editors, Certified Programs and Proofs (CPP), pages 125-137. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018621.
  12. Milad Ketab Ghale, Dirk Pattinson, and Ramana Kumar. Verified certificate checking for counting votes. In Ruzica Piskac and Philipp Rümmer, editors, Verified Software. Theories, Tools, and Experiments (VSTTE), volume 11294 of LNCS. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03592-1_5.
  13. Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. Verified characteristic formulae for CakeML. In Hongseok Yang, editor, European Symposium on Programming (ESOP), volume 10201 of LNCS. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_22.
  14. Alejandro Gómez-Londoño. Choreographies and cost semantics for reliable communicating systems, 2020. Licentiate thesis, Chalmers University of Technology. Google Scholar
  15. Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan. Do you have space for dessert? A verified space cost semantics for CakeML programs. Proc. ACM Program. Lang. (OOPSLA), 4:204:1-204:29, 2020. URL: https://doi.org/10.1145/3428272.
  16. Rikard Hjort, Jakob Holmgren, and Christian Persson. The CakeML compiler explorer - tracking intermediate representations in a verified compiler. In Meng Wang and Scott Owens, editors, Trends in Functional Programming (TFP), volume 10788 of LNCS, pages 135-148. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-89719-6_8.
  17. Lars Hupel and Tobias Nipkow. A verified compiler from Isabelle/HOL to CakeML. In Amal Ahmed, editor, European Symposium on Programming (ESOP), volume 10801 of LNCS, pages 999-1026. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_35.
  18. Ramana Kumar. Self-compilation and self-verification. PhD thesis, University of Cambridge, 2016. Google Scholar
  19. Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. HOL with definitions: Semantics, soundness, and a verified implementation. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving (ITP), volume 8558 of LNCS, pages 308-324. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_20.
  20. Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. Self-formalisation of higher-order logic - semantics, soundness, and a verified implementation. Journal of Automated Reasoning (JAR), 56(3):221-259, 2016. URL: https://doi.org/10.1007/s10817-015-9357-x.
  21. Ramana Kumar, Eric Mullen, Zachary Tatlock, and Magnus O. Myreen. Software verification with ITPs should use binary code extraction to reduce the TCB (short paper). In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving (ITP), volume 10895 of LNCS, pages 362-369. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_21.
  22. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, Principles of Programming Languages (POPL). ACM, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  23. Ramana Kumar and Michael Norrish. (nominal) unification by recursive descent with triangular substitutions. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of LNCS, pages 51-66. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_6.
  24. Andreas Lööw. Lutsig: a verified Verilog compiler for verified circuit development. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 46-60. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439916.
  25. Andreas Lööw and Magnus O. Myreen. A proof-producing translator for Verilog development in HOL. In Stefania Gnesi, Nico Plat, Nancy A. Day, and Matteo Rossi, editors, Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019, pages 99-108. IEEE / ACM, 2019. URL: https://doi.org/10.1109/FormaliSE.2019.00020.
  26. Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. Verified compilation on a verified processor. In Programming Language Design and Implementation (PLDI). ACM, 2019. URL: https://doi.org/10.1145/3314221.3314622.
  27. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: reusable engineering of real-world semantics. In Johan Jeuring and Manuel M. T. Chakravarty, editors, International Conference on Functional Programming (ICFP). ACM, 2014. URL: https://doi.org/10.1145/2628136.2628143.
  28. Magnus O. Myreen. Formal verification of machine-code programs. PhD thesis, University of Cambridge, 2009. Google Scholar
  29. Magnus O. Myreen. Verified just-in-time compiler on x86. In Manuel V. Hermenegildo and Jens Palsberg, editors, Principles of Programming Languages (POPL). ACM, 2010. Google Scholar
  30. Magnus O. Myreen. A minimalistic verified bootstrapped compiler (proof pearl). In Catalin Hritcu and Andrei Popescu, editors, Conference on Certified Programs and Proofs (CPP), pages 32-45. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439915.
  31. Magnus O. Myreen and Gregorio Curello. Proof pearl: A verified bignum implementation in x86-64 machine code. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs (CPP), volume 8307 of LNCS, pages 66-81. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_5.
  32. Magnus O. Myreen and Scott Owens. Proof-producing synthesis of ML from higher-order logic. In International Conference on Functional Programming (ICFP), pages 115-126. ACM Press, 2012. URL: https://doi.org/10.1145/2364527.2364545.
  33. Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. Journal of Functional Programming (JFP), 24(2-3):284-315, 2014. URL: https://doi.org/10.1017/S0956796813000282.
  34. Magnus O. Myreen, Scott Owens, and Ramana Kumar. Steps towards verified implementations of HOL light. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 490-495. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_38.
  35. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In Peter Thiemann, editor, European Symposium on Programming (ESOP), LNCS. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_23.
  36. Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan. Verifying efficient function calls in CakeML. Proc. ACM Program. Lang., 1(ICFP), September 2017. URL: https://doi.org/10.1145/3110262.
  37. Johannes Aman Pohjola and Arve Gengelbach. A mechanised semantics for HOL with ad-hoc overloading. In Elvira Albert and Laura Kovacs, editors, Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 73 of EPiC Series in Computing, pages 498-515. EasyChair, 2020. Google Scholar
  38. Konrad Slind. Specifying message formats with contiguity types. In Interactive Theorem Proving (ITP), Leibniz International Proceedings in Informatics. Schloss Dagstuhl Leibniz-Zentrum für Informatik, Dagstuhl Publishing, 2021. Google Scholar
  39. Konrad Slind, David S. Hardin, Johannes Åman Pohjola, and Michael Sproul. Synthesis of verified architectural components for autonomy hosted on a verified microkernel. In Hawaii International Conference on System Sciences, January 2020. Google Scholar
  40. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified propagation redundancy checking in CakeML. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_12.
  41. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming, 29, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  42. Yong Kiam Tan, Scott Owens, and Ramana Kumar. A verified type system for CakeML. In Implementation and Application of Functional Programming Languages (IFL). ACM Press, 2015. URL: https://doi.org/10.1145/2897336.2897344.
  43. Thomas Tuerk, Magnus O. Myreen, and Ramana Kumar. Pattern matches in HOL: A new representation and improved code generation. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving (ITP), volume 9236 of LNCS, pages 453-468. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_30.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact