CakeML Publications
The canonical references:
- for the CakeML project as a whole: this POPL 2014 paper with bibtex
- for the CakeML compiler: this JFP paper with bibtex
- for the PureCake compiler: this PLDI 2023 paper with bibtex
- for the Candle theorem prover: this ITP 2022 paper with bibtex
A timeline of the CakeML work up to 2021 is described in this ITP 2021 extended abstract.
All CakeML related publications (that we know of)
| [1] | Hrutvik Kanabar, Kacper Korban, and Magnus O. Myreen. Verified inlining and specialisation for PureCake. In Stephanie Weirich, editor, European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, 2024. To appear. [ bib | .pdf ] |
| [2] | Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, and Jakob Nordström. Certified MaxSAT preprocessing. In International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Computer Science. Springer, 2024. To appear. [ bib ] |
| [3] | Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Formally certified approximate model counting. In Computer Aided Verification (CAV), Lecture Notes in Computer Science. Springer, 2024. To appear. [ bib ] |
| [4] | Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-end verification for subgraph solving. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, Artificial Intelligence (AAAI). AAAI Press, 2024. [ bib | DOI | .pdf ] |
| [5] | Oskar Abrahamsson and Magnus O. Myreen. Fast, verified computation for Candle. In Interactive Theorem Proving (ITP). LIPIcs, 2023. [ bib | .pdf ] |
| [6] | Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, and Scott Owens. Cakes that bake cakes: Dynamic computation in CakeML. In Programming Language Design and Implementation (PLDI). ACM, 2023. [ bib | .pdf ] |
| [7] | Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, and Riccardo Zanetti. PureCake: A verified compiler for a lazy functional language. In Programming Language Design and Implementation (PLDI). ACM, 2023. [ bib | .pdf ] |
| [8] | Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. Verified propagation redundancy and compositional UNSAT checking in CakeML. Journal on Software Tools for Technology Transfer (STTT), 2023. [ bib | http ] |
| [9] | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A verified implementation of HOL Light. In Interactive Theorem Proving (ITP). LIPIcs, 2022. [ bib | .pdf ] |
| [10] | Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen. Taming an authoritative Armv8 ISA specification: L3 validation and CakeML compiler verification. In Interactive Theorem Proving (ITP). LIPIcs, 2022. [ bib | .pdf ] |
| [11] | Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified compilation and optimization of floating-point programs in CakeML. In European Conference on Object-Oriented Programming (ECOOP). LIPIcs, 2022. [ bib | .pdf ] |
| [12] | Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A verified, end-to-end compiler for a choreographic language. In Interactive Theorem Proving (ITP). LIPIcs, 2022. [ bib | .pdf ] |
| [13] | 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. [ bib | DOI | .pdf ] |
| [14] | Andreas Lööw. Lutsig: a verified Verilog compiler for verified circuit development. In Catalin Hritcu and Andrei Popescu, editors, Conference on Certified Programs and Proofs (CPP), pages 46--60. ACM, 2021. [ bib | DOI | .pdf ] |
| [15] | 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. [ bib | .pdf ] |
| [16] | Magnus O. Myreen. The CakeML project’s quest for ever stronger correctness theorems. In Interactive Theorem Proving (ITP). LIPIcs, 2021. [ bib | .pdf ] |
| [17] | 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. [ bib | DOI | .pdf ] |
| [18] | Oskar Abrahamsson. A verified proof checker for higher-order logic. Journal of Logical and Algebraic Methods in Programming, 112:100530, 2020. [ bib | DOI | .pdf ] |
| [19] | Johannes Åman 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. [ bib | http ] |
| [20] | 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. [ bib | http ] |
| [21] | Adam Sandberg Ericsson, Magnus O. Myreen, and Johannes Åman Pohjola. A verified generational garbage collector for CakeML. Journal of Automated Reasoning (JAR), 63, 2019. [ bib | DOI | .pdf ] |
| [22] | 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. [ bib | DOI | .pdf ] |
| [23] | 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. [ bib | DOI | .pdf ] |
| [24] | 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. [ bib | .pdf ] |
| [25] | Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic formulae for liveness properties of non-terminating CakeML programs. In Interactive Theorem Proving (ITP). LIPICS, 2019. [ bib | .pdf ] |
| [26] | 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. [ bib | .pdf ] |
| [27] | 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 Lecture Notes in Computer Science. Springer, 2018. [ bib | DOI | http ] |
| [28] | 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 Ruzica Piskac and Philipp Rümmer, editors, Verified Software. Theories, Tools, and Experiments (VSTTE), volume 11294 of Lecture Notes in Computer Science. Springer, 2018. [ bib | DOI | .pdf ] |
| [29] | 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. [ bib | DOI | .pdf ] |
| [30] | 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 Lecture Notes in Computer Science, pages 362--369. Springer, 2018. [ bib | DOI | .pdf ] |
| [31] | 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), volume 10900 of Lecture Notes in Computer Science, pages 646--662. Springer, 2018. [ bib | DOI | .pdf ] |
| [32] | 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 Lecture Notes in Computer Science, pages 999--1026. Springer, 2018. [ bib | DOI | .pdf ] |
| [33] | 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. [ bib | DOI | .pdf ] |
| [34] | 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 Lecture Notes in Computer Science, pages 135--148. Springer, 2017. [ bib | DOI | http ] |
| [35] | 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 Lecture Notes in Computer Science, pages 118--134. Springer, 2017. [ bib | DOI | http ] |
| [36] | Adam Sandberg Ericsson, Magnus O. Myreen, and Johannes Åman Pohjola. A verified generational garbage collector for CakeML. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving (ITP), volume 10499 of Lecture Notes in Computer Science, pages 444--461. Springer, 2017. [ bib | DOI | .pdf ] |
| [37] | 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. [ bib | DOI | .pdf ] |
| [38] | 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 Lecture Notes in Computer Science, pages 584--610. Springer, 2017. [ bib | DOI | .pdf ] |
| [39] | Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. A new verified compiler backend for CakeML. In International Conference on Functional Programming (ICFP), pages 60--73. ACM Press, September 2016. Invited to special issue of Journal of Functional Programming. [ bib | DOI | .pdf ] |
| [40] | Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In Peter Thiemann, editor, European Symposium on Programming (ESOP), volume 9632 of Lecture Notes in Computer Science, pages 589--615. Springer, April 2016. [ bib | DOI | .pdf ] |
| [41] | 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. [ bib | DOI | .pdf ] |
| [42] | 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 Lecture Notes in Computer Science, pages 453--468. Springer, 2015. [ bib | DOI | .pdf ] |
| [43] | Benja Fallenstein and Ramana Kumar. Proof-producing reflection for HOL - with an application to model polymorphism. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 170--186. Springer, 2015. [ bib | DOI | .pdf ] |
| [44] | 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. Awarded the Peter Landin prize for best paper. [ bib | DOI | .pdf ] |
| [45] | 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 Lecture Notes in Computer Science, pages 308--324. Springer, July 2014. [ bib | DOI | .pdf ] |
| [46] | 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, May 2014. [ bib | DOI | .pdf ] |
| [47] | Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Principles of Programming Languages (POPL), pages 179--191. ACM Press, January 2014. [ bib | DOI | .pdf ] |
| [48] | 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 Lecture Notes in Computer Science, pages 66--81. Springer, 2013. [ bib | DOI | .pdf ] |
| [49] | 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 Lecture Notes in Computer Science, pages 490--495. Springer, 2013. [ bib | DOI | http ] |
| [50] | 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, September 2012. [ bib | DOI | .html ] |
This file was generated by bibtex2html 1.99.