@inproceedings{LasnierYM26,
author = {Pascal Y. Lasnier and Jeremy Yallop and Magnus O. Myreen},
editor = {Kathrin Stark and Yannick Zakowski and Nikhil Swamy and Nicolas Tabareau},
title = {Brack: {A} Verified Compiler for Scheme via CakeML},
booktitle = {Certified Programs and Proofs {(CPP)}},
pages = {157--170},
publisher = {{ACM}},
year = {2026},
url = {https://doi.org/10.1145/3779031.3779098},
doi = {10.1145/3779031.3779098},
timestamp = {Tue, 03 Feb 2026 08:27:35 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LasnierYM26.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{NezamabadiMT26,
author = {Daniel Nezamabadi and Magnus O. Myreen and Yong Kiam Tan},
editor = {Kathrin Stark and Yannick Zakowski and Nikhil Swamy and Nicolas Tabareau},
title = {Verified {VCG} and Verified Compiler for Dafny},
booktitle = {Certified Programs and Proofs {(CPP)}},
pages = {171--186},
publisher = {{ACM}},
year = {2026},
url = {https://doi.org/10.1145/3779031.3779092},
doi = {10.1145/3779031.3779092},
timestamp = {Tue, 03 Feb 2026 08:27:35 +0100},
biburl = {https://dblp.org/rec/conf/cpp/NezamabadiMT26.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{LasnierYM25,
author = {Pascal Y. Lasnier and Jeremy Yallop and Magnus O. Myreen},
editor = {Nada Amin and Joaquin Arias},
title = {A One-Pass {CPS} Transform with Simulation on the Nose},
booktitle = {Practical Aspects of Declarative Languages {(PADL)}},
series = {LNCS},
volume = {16401},
pages = {21--38},
publisher = {Springer},
year = {2026},
url = {https://doi.org/10.1007/978-3-032-15981-6_2},
doi = {10.1007/978-3-032-15981-6_2},
timestamp = {Mon, 27 Apr 2026 07:31:12 +0200},
biburl = {https://dblp.org/rec/conf/padl/LasnierYM25.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{dold_et_al:LIPIcs.CP.2026.21,
author = {Dold, Simon and Katsirelos, George and Koops, Wietze and Myreen, Magnus O. and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam},
title = {{End-to-End Certified Graph Colouring}},
booktitle = {Principles and Practice of Constraint Programming (CP 2026)},
pages = {21:1--21:27},
series = {LIPIcs},
isbn = {978-3-95977-432-1},
issn = {1868-8969},
year = {2026},
volume = {379},
editor = {Beldiceanu, Nicolas},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.21},
urn = {urn:nbn:de:0030-drops-266546},
doi = {10.4230/LIPIcs.CP.2026.21},
annote = {Keywords: graph colouring, proof logging, certifying algorithms}
}
@inproceedings{Koops25,
author = {Wietze Koops and Daniel Le Berre and Magnus O. Myreen and Jakob Nordstr{\"{o}}m and Andy Oertel and Yong Kiam Tan and Marc Vinyals},
editor = {Maria Garcia de la Banda},
title = {Practically Feasible Proof Logging for Pseudo-Boolean Optimization},
booktitle = {Principles and Practice of Constraint Programming ({CP})},
series = {LIPIcs},
volume = {340},
pages = {21:1--21:27},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2025},
url = {https://doi.org/10.4230/LIPIcs.CP.2025.21},
doi = {10.4230/LIPICS.CP.2025.21}
}
@inproceedings{yang_et_al:LIPIcs.SAT.2025.32,
author = {Yang, Jiong and Tan, Yong Kiam and Soos, Mate and Myreen, Magnus O. and Meel, Kuldeep S.},
title = {{Efficient Certified Reasoning for Binarized Neural Networks}},
booktitle = {Theory and Applications of Satisfiability Testing (SAT)},
pages = {32:1--32:22},
series = {LIPIcs},
isbn = {978-3-95977-381-2},
issn = {1868-8969},
year = {2025},
volume = {341},
comeditor = {Berg, Jeremias and Nordstr\"{o}m, Jakob},
publisher = {Schloss Dagstuhl},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.32},
urn = {urn:nbn:de:0030-drops-237665},
doi = {10.4230/LIPIcs.SAT.2025.32}
}
@inproceedings{AAAI24,
author = {Stephan Gocht and Ciaran McCreesh and Magnus O. Myreen and Jakob Nordstr{\"{o}}m and Andy Oertel and Yong Kiam Tan},
editor = {Michael J. Wooldridge and Jennifer G. Dy and Sriraam Natarajan},
title = {End-to-End Verification for Subgraph Solving},
booktitle = {Artificial Intelligence ({AAAI})},
publisher = {{AAAI} Press},
year = {2024},
url = {aaai24-verified-subgraphs.pdf},
doi = {10.1609/AAAI.V38I8.28642}
}
@inproceedings{CAV24,
author = {Yong Kiam Tan and Jiong Yang and Mate Soos and Magnus O. Myreen and Kuldeep S. Meel},
editor = {Arie Gurfinkel and Vijay Ganesh},
title = {Formally Certified Approximate Model Counting},
booktitle = {Computer Aided Verification ({CAV})},
volume = {14681},
pages = {153--177},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-65627-9_8},
doi = {10.1007/978-3-031-65627-9_8},
note = {Distinguished Paper}
}
@inproceedings{IJCAR24,
author = {Hannes Ihalainen and Andy Oertel and Yong Kiam Tan and Jeremias Berg and Matti J{\"{a}}rvisalo and Magnus O. Myreen and Jakob Nordstr{\"{o}}m},
title = {Certified {MaxSAT} Preprocessing},
year = {2024},
booktitle = {International Joint Conference on Automated Reasoning ({IJCAR})},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
url = {ijcar24_CertifiedMaxSATpreprocessing.pdf}
}
@inproceedings{ESOP24,
author = {Kanabar, Hrutvik and Korban, Kacper and Myreen, Magnus O.},
title = {Verified Inlining and Specialisation for {PureCake}},
year = {2024},
booktitle = {European Symposium on Programming ({ESOP})},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
editor = {Stephanie Weirich},
url = {esop24-inlining.pdf}
}
@article{STTT23,
author = {Yong Kiam Tan and Marijn J. H. Heule and Magnus O. Myreen},
title = {Verified Propagation Redundancy and Compositional {UNSAT} Checking in {CakeML}},
journal = {Journal on Software Tools for Technology Transfer {(STTT)}},
publisher = {Springer},
year = {2023},
url = {https://trebuchet.public.springernature.app/get_content/412ab5ed-7746-4a59-a167-39decba811d8}
}
@inproceedings{PLDI23PureCake,
author = {Hrutvik Kanabar and Samuel Vivien and Oskar Abrahamsson and Magnus O. Myreen and Michael Norrish and Johannes Åman Pohjola and Riccardo Zanetti},
title = {{PureCake}: A Verified Compiler for a Lazy Functional Language},
year = 2023,
booktitle = {Programming Language Design and Implementation (PLDI)},
publisher = {ACM},
url = {pldi23-purecake.pdf}
}
@inproceedings{PLDI23Eval,
author = {Thomas Sewell and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar and Alexander Mihajlovic and Oskar Abrahamsson and Scott Owens},
title = {Cakes that Bake Cakes: Dynamic Computation in {CakeML}},
year = 2023,
booktitle = {Programming Language Design and Implementation (PLDI)},
publisher = {ACM},
url = {pldi23-eval.pdf}
}
@inproceedings{ITP23,
author = {Oskar Abrahamsson and Magnus O. Myreen},
title = {Fast, Verified Computation for {Candle}},
year = 2023,
booktitle = {Interactive Theorem Proving ({ITP})},
publisher = {LIPIcs},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18379/pdf/LIPIcs-ITP-2023-4.pdf}
}
@inproceedings{ITP22kalas,
author = {Johannes Åman Pohjola and Alejandro Gómez-Londoño and James Shaker and Michael Norrish},
title = {Kalas: A Verified, End-To-End Compiler for a Choreographic Language},
year = 2022,
booktitle = {Interactive Theorem Proving ({ITP})},
publisher = {LIPIcs},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16736/pdf/LIPIcs-ITP-2022-27.pdf}
}
@inproceedings{ECOOP22,
author = {Heiko Becker and Robert Rabe and Eva Darulova and Magnus O. Myreen and Zachary Tatlock and Ramana Kumar and Yong Kiam Tan and Anthony Fox},
title = {Verified Compilation and Optimization of Floating-Point Programs in {CakeML}},
year = 2022,
booktitle = {European Conference on Object-Oriented Programming ({ECOOP})},
publisher = {LIPIcs},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16229/pdf/LIPIcs-ECOOP-2022-1.pdf}
}
@inproceedings{ITP21,
author = {Magnus O. Myreen},
title = {The {CakeML} Project’s Quest for Ever Stronger Correctness Theorems},
year = 2021,
booktitle = {Interactive Theorem Proving ({ITP})},
publisher = {LIPIcs},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13896/pdf/LIPIcs-ITP-2021-1.pdf}
}
@inproceedings{ITP22armv8,
author = {Hrutvik Kanabar and Anthony C. J. Fox and Magnus O. Myreen},
title = {Taming an Authoritative {Armv8} {ISA} Specification: {L3} Validation and {CakeML} Compiler Verification},
year = 2022,
booktitle = {Interactive Theorem Proving ({ITP})},
publisher = {LIPIcs},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16729/pdf/LIPIcs-ITP-2022-20.pdf}
}
@inproceedings{ITP22candle,
author = {Oskar Abrahamsson and Magnus O. Myreen and Ramana Kumar and Thomas Sewell},
title = {{Candle}: A Verified Implementation of {HOL} {Light}},
year = 2022,
booktitle = {Interactive Theorem Proving ({ITP})},
publisher = {LIPIcs},
url = {https://drops.dagstuhl.de/opus/volltexte/2022/16712/pdf/LIPIcs-ITP-2022-3.pdf}
}
@inproceedings{TACAS21,
author = {Yong Kiam Tan and Marijn J. H. Heule and Magnus O. Myreen},
title = {cake_lpr: Verified Propagation Redundancy Checking in {CakeML}},
year = 2021,
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})},
publisher = {Springer},
url = {https://cakeml.org/tacas21.pdf}
}
@article{ComputeJAR25,
author = {Oskar Abrahamsson and Magnus O. Myreen and Michael Norrish and Hrutvik Kanabar and Johannes Åman Pohjola},
title = {Fast, Verified Computation for {HOL} {ITPs}},
journal = {Journal of Automated Reasoning ({JAR})},
publisher = {Springer},
year = {2025},
url = {https://rdcu.be/eTh70}
}
@article{CandleJAR25,
author = {Oskar Abrahamsson and Ramana Kumar and Magnus O. Myreen and Thomas Sewell},
title = {Candle: A Verified Implementation of {HOL Light} (Extended Version)},
journal = {Journal of Automated Reasoning ({JAR})},
publisher = {Springer},
year = {2025},
url = {https://rdcu.be/eTh5c}
}
@article{JAR20,
author = {Oskar Abrahamsson and Son Ho and Hrutvik Kanabar and Ramana Kumar and Magnus O. Myreen and Michael Norrish and Yong Kiam Tan},
title = {Proof-Producing Synthesis of {CakeML} from Monadic {HOL} Functions},
journal = {Journal of Automated Reasoning ({JAR})},
publisher = {Springer},
year = {2020},
url = {https://rdcu.be/b4FrU}
}
@inproceedings{PohjolaG20,
author = {Johannes Åman Pohjola and Arve Gengelbach},
editor = {Elvira Albert and Laura Kovacs},
title = {A Mechanised Semantics for {HOL} with Ad-hoc Overloading},
booktitle = {Logic for Programming, Artificial Intelligence and Reasoning (LPAR)},
series = {EPiC Series in Computing},
volume = {73},
pages = {498--515},
publisher = {EasyChair},
year = {2020},
url = {https://easychair.org/publications/download/9Hcd}
}
@inproceedings{Loow21,
author = {Andreas Lööw},
editor = {Catalin Hritcu and Andrei Popescu},
title = {{Lutsig}: a verified {Verilog} compiler for verified circuit development},
booktitle = {Conference on Certified Programs and Proofs (CPP)},
pages = {46--60},
publisher = {{ACM}},
year = {2021},
url = {cpp21.pdf},
doi = {10.1145/3437992.3439916}
}
@inproceedings{Myreen21,
author = {Magnus O. Myreen},
editor = {Catalin Hritcu and Andrei Popescu},
title = {A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)},
booktitle = {Conference on Certified Programs and Proofs (CPP)},
pages = {32--45},
publisher = {{ACM}},
year = {2021},
url = {http://www.cse.chalmers.se/~myreen/cpp2021-bootstrap-myreen.pdf},
doi = {10.1145/3437992.3439915}
}
@article{JLAMP20,
author = {Oskar Abrahamsson},
title = {A Verified Proof Checker for Higher-Order Logic},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {112},
pages = {100530},
year = {2020},
url = {https://cakeml.org/jlamp20.pdf},
doi = {10.1016/j.jlamp.2020.100530}
}
@inproceedings{ITP19,
author = {Johannes Åman Pohjola and Henrik Rostedt and Magnus O. Myreen},
title = {Characteristic Formulae for Liveness Properties of Non-terminating {CakeML} Programs},
year = 2019,
booktitle = {Interactive Theorem Proving ({ITP})},
publisher = {LIPICS},
url = {https://cakeml.org/itp19.pdf}
}
@inproceedings{CAV19,
author = {Heiko Becker and Eva Darulova and Magnus O. Myreen and Zachary Tatlock},
title = {Icing: Supporting Fast-math Style Optimizations in a Verified Compiler},
year = 2019,
booktitle = {Computer Aided Verification ({CAV})},
publisher = {Springer},
url = {https://cakeml.org/cav19.pdf}
}
@inproceedings{PLDI19,
author = {Andreas Lööw and Ramana Kumar and Yong Kiam Tan and Magnus O. Myreen and Michael Norrish and Oskar Abrahamsson and Anthony Fox},
title = {Verified Compilation on a Verified Processor},
year = 2019,
booktitle = {Programming Language Design and Implementation ({PLDI})},
publisher = {{ACM}},
url = {https://cakeml.org/pldi19.pdf},
doi = {10.1145/3314221.3314622}
}
@article{jfp2019,
title = {The verified {CakeML} compiler backend},
journal = {Journal of Functional Programming},
volume = {29},
publisher = {Cambridge University Press},
author = {Yong Kiam Tan and Magnus O. Myreen and Ramana Kumar and Anthony Fox and Scott Owens and Michael Norrish},
year = {2019},
url = {jfp19.pdf},
doi = {10.1017/S0956796818000229}
}
@inproceedings{ESOP16,
author = {Scott Owens and Magnus O. Myreen and Ramana Kumar and Yong Kiam Tan},
title = {Functional Big-step Semantics},
year = 2016,
month = apr,
booktitle = {European Symposium on Programming ({ESOP})},
publisher = {Springer},
volume = 9632,
series = {Lecture Notes in Computer Science},
editor = {Peter Thiemann},
pages = {589--615},
url = {https://cakeml.org/esop16.pdf},
doi = {10.1007/978-3-662-49498-1_23}
}
@inproceedings{ICFP12,
author = {Magnus O. Myreen and Scott Owens},
title = {Proof-Producing Synthesis of {ML} from Higher-Order Logic},
booktitle = {International Conference on Functional Programming ({ICFP})},
pages = {115--126},
year = 2012,
month = sep,
publisher = {ACM Press},
url = {https://cakeml.org/icfp12/index.html},
doi = {10.1145/2364527.2364545}
}
@inproceedings{ICFP16,
author = {Yong Kiam Tan and Magnus O. Myreen and Ramana Kumar and Anthony Fox and Scott Owens and Michael Norrish},
title = {A New Verified Compiler Backend for {CakeML}},
booktitle = {International Conference on Functional Programming ({ICFP})},
pages = {60--73},
year = 2016,
month = sep,
publisher = {ACM Press},
doi = {10.1145/2951913.2951924},
url = {https://cakeml.org/icfp16.pdf},
note = {Invited to special issue of Journal of Functional Programming}
}
@article{ICFP17,
author = {Scott Owens and Michael Norrish and Ramana Kumar and Magnus O. Myreen and Yong Kiam Tan},
title = {Verifying Efficient Function Calls in {CakeML}},
journal = {Proc. ACM Program. Lang.},
articleno = {18},
numpages = {27},
year = 2017,
volume = 1,
number = {ICFP},
month = sep,
publisher = {ACM Press},
url = {https://cakeml.org/icfp17.pdf},
doi = {10.1145/3110262}
}
@inproceedings{IFL15a,
author = {Yong Kiam Tan and Scott Owens and Ramana Kumar},
title = {A Verified Type System for {CakeML}},
booktitle = {Implementation and Application of Functional Programming Languages ({IFL})},
year = 2015,
publisher = {ACM Press},
doi = {10.1145/2897336.2897344},
url = {https://cakeml.org/ifl15.pdf},
note = {Awarded the Peter Landin prize for best paper}
}
@inproceedings{ITP14,
author = {Ramana Kumar and Rob Arthan and Magnus O. Myreen and Scott Owens},
title = {{HOL} with Definitions: Semantics, Soundness, and a Verified Implementation},
booktitle = {Interactive Theorem Proving ({ITP})},
editor = {Gerwin Klein and Ruben Gamboa},
volume = 8558,
year = 2014,
pages = {308--324},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
month = jul,
url = {https://cakeml.org/itp14.pdf},
doi = {10.1007/978-3-319-08970-6_20}
}
@article{JFP14,
author = {Magnus O. Myreen and Scott Owens},
title = {Proof-producing Translation of Higher-order logic into Pure and Stateful {ML}},
journal = {Journal of Functional Programming ({JFP})},
volume = 24,
number = {2-3},
pages = {284--315},
month = may,
year = 2014,
url = {https://cakeml.org/jfp14.pdf},
doi = {10.1017/S0956796813000282}
}
@inproceedings{POPL14,
author = {Ramana Kumar and Magnus O. Myreen and Michael Norrish and Scott Owens},
title = {{CakeML}: A Verified Implementation of {ML}},
month = jan,
year = 2014,
pages = {179--191},
publisher = {ACM Press},
url = {https://cakeml.org/popl14.pdf},
booktitle = {Principles of Programming Languages ({POPL})},
doi = {10.1145/2535838.2535841}
}
@inproceedings{ITP13,
author = {Magnus O. Myreen and Scott Owens and Ramana Kumar},
title = {Steps towards Verified Implementations of {HOL} {Light}},
booktitle = {Interactive Theorem Proving ({ITP})},
pages = {490--495},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2_38},
doi = {10.1007/978-3-642-39634-2_38},
series = {Lecture Notes in Computer Science},
volume = {7998},
publisher = {Springer},
editor = {Sandrine Blazy and Christine Paulin{-}Mohring and David Pichardie}
}
@inproceedings{ITP15,
author = {Benja Fallenstein and Ramana Kumar},
title = {Proof-Producing Reflection for {HOL} - With an Application to Model
Polymorphism},
editor = {Christian Urban and Xingyuan Zhang},
booktitle = {Interactive Theorem Proving ({ITP})},
series = {Lecture Notes in Computer Science},
volume = {9236},
publisher = {Springer},
pages = {170--186},
year = {2015},
url = {https://cakeml.org/itp15-reflection.pdf},
doi = {10.1007/978-3-319-22102-1_11}
}
@inproceedings{ITP15pmatch,
author = {Thomas Tuerk and Magnus O. Myreen and Ramana Kumar},
title = {Pattern Matches in {HOL:} {A} New Representation and Improved Code
Generation},
booktitle = {Interactive Theorem Proving ({ITP})},
editor = {Christian Urban and Xingyuan Zhang},
pages = {453--468},
year = {2015},
series = {Lecture Notes in Computer Science},
volume = {9236},
publisher = {Springer},
url = {https://cakeml.org/itp15-pmatch.pdf},
doi = {10.1007/978-3-319-22102-1_30}
}
@article{JAR16,
author = {Ramana Kumar and Rob Arthan and Magnus O. Myreen and Scott Owens},
title = {Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and
a Verified Implementation},
journal = {Journal of Automated Reasoning ({JAR})},
publisher = {Springer},
volume = {56},
number = {3},
pages = {221--259},
year = {2016},
url = {https://cakeml.org/jarhol.pdf},
doi = {10.1007/s10817-015-9357-x}
}
@article{JAR19,
author = {Adam Sandberg Ericsson and Magnus O. Myreen and Johannes Åman Pohjola},
title = {A Verified Generational Garbage Collector for {CakeML}},
year = {2019},
url = {https://link.springer.com/content/pdf/10.1007%2Fs10817-018-9487-z.pdf},
journal = {Journal of Automated Reasoning ({JAR})},
volume = {63},
publisher = {Springer},
doi = {10.1007/s10817-018-9487-z}
}
@inproceedings{ESOP17,
author = {Armaël Guéneau and Magnus O. Myreen and Ramana Kumar and Michael Norrish},
title = {Verified Characteristic Formulae for {CakeML}},
booktitle = {European Symposium on Programming ({ESOP})},
editor = {Hongseok Yang},
pages = {584--610},
series = {Lecture Notes in Computer Science},
volume = {10201},
publisher = {Springer},
year = {2017},
url = {https://cakeml.org/esop17.pdf},
doi = {10.1007/978-3-662-54434-1_22}
}
@inproceedings{CPP17,
author = {Anthony C. J. Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar},
title = {Verified compilation of {CakeML} to multiple machine-code targets},
booktitle = {Certified Programs and Proofs ({CPP})},
editor = {Yves Bertot and Viktor Vafeiadis},
pages = {125--137},
year = {2017},
publisher = {{ACM}},
url = {https://cakeml.org/cpp17.pdf},
doi = {10.1145/3018610.3018621}
}
@inproceedings{ITP17,
author = {Adam Sandberg Ericsson and Magnus O. Myreen and Johannes Åman Pohjola},
title = {A Verified Generational Garbage Collector for {CakeML}},
booktitle = {Interactive Theorem Proving ({ITP})},
pages = {444--461},
year = {2017},
url = {https://cakeml.org/itp17.pdf},
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and C{\'{e}}sar A. Mu{\~{n}}oz},
series = {Lecture Notes in Computer Science},
volume = {10499},
publisher = {Springer},
doi = {10.1007/978-3-319-66107-0_28}
}
@inproceedings{TFP17tailrec,
author = {Oskar Abrahamsson and Magnus O. Myreen},
title = {Automatically Introducing Tail Recursion in {CakeML}},
booktitle = {Trends in Functional Programming ({TFP})},
editor = {Meng Wang and Scott Owens},
series = {Lecture Notes in Computer Science},
volume = {10788},
publisher = {Springer},
pages = {118--134},
year = {2017},
url = {https://link.springer.com/chapter/10.1007/978-3-319-89719-6_7},
doi = {10.1007/978-3-319-89719-6_7}
}
@inproceedings{TFP17explorer,
author = {Rikard Hjort and Jakob Holmgren and Christian Persson},
title = {The {CakeML} Compiler Explorer - Tracking Intermediate Representations
in a Verified Compiler},
booktitle = {Trends in Functional Programming ({TFP})},
editor = {Meng Wang and Scott Owens},
series = {Lecture Notes in Computer Science},
volume = {10788},
publisher = {Springer},
pages = {135--148},
year = {2017},
url = {https://link.springer.com/chapter/10.1007/978-3-319-89719-6_8},
doi = {10.1007/978-3-319-89719-6_8}
}
@inproceedings{ESOP18,
author = {Lars Hupel and Tobias Nipkow},
title = {A Verified Compiler from {Isabelle/HOL} to {CakeML}},
booktitle = {European Symposium on Programming ({ESOP})},
pages = {999--1026},
series = {Lecture Notes in Computer Science},
volume = {10801},
publisher = {Springer},
editor = {Amal Ahmed},
year = {2018},
url = {https://lars.hupel.info/pub/isabelle-cakeml.pdf},
doi = {10.1007/978-3-319-89884-1_35}
}
@inproceedings{CPP13,
author = {Magnus O. Myreen and Gregorio Curello},
title = {Proof Pearl: {A} Verified Bignum Implementation in x86-64 Machine
Code},
booktitle = {Certified Programs and Proofs ({CPP})},
editor = {Georges Gonthier and Michael Norrish},
series = {Lecture Notes in Computer Science},
volume = {8307},
publisher = {Springer},
pages = {66--81},
year = {2013},
url = {http://www.cse.chalmers.se/~myreen/cpp13.pdf},
doi = {10.1007/978-3-319-03545-1_5}
}
@inproceedings{IJCAR18,
author = {Son Ho and Oskar Abrahamsson and Ramana Kumar and Magnus O. Myreen and Yong Kiam Tan and Michael Norrish},
title = {Proof-Producing Synthesis of {CakeML} with {I/O} and Local State from
Monadic {HOL} Functions},
booktitle = {Automated Reasoning - 9th International Joint Conference ({IJCAR})},
editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
series = {Lecture Notes in Computer Science},
volume = {10900},
publisher = {Springer},
pages = {646--662},
year = {2018},
url = {https://cakeml.org/ijcar18.pdf},
doi = {10.1007/978-3-319-94205-6_42}
}
@inproceedings{ITP18,
author = {Ramana Kumar and Eric Mullen and Zachary Tatlock and Magnus O. Myreen},
title = {Software Verification with {ITPs} Should Use Binary Code Extraction
to Reduce the {TCB} (Short Paper)},
booktitle = {Interactive Theorem Proving ({ITP})},
editor = {Jeremy Avigad and Assia Mahboubi},
series = {Lecture Notes in Computer Science},
volume = {10895},
publisher = {Springer},
pages = {362--369},
year = {2018},
url = {https://cakeml.org/itp18-short.pdf},
doi = {10.1007/978-3-319-94821-8_21}
}
@inproceedings{PLDI18,
author = {Brandon Bohrer and Yong Kiam Tan and Stefan Mitsch and Magnus O. Myreen and André Platzer},
title = {{VeriPhy}: verified controller executables from verified cyber-physical
system models},
booktitle = {Programming Language Design and Implementation ({PLDI})},
editor = {Jeffrey S. Foster and Dan Grossman},
publisher = {{ACM}},
pages = {617--630},
year = {2018},
url = {http://www.cs.cmu.edu/~bbohrer/pub/pldi18.pdf},
doi = {10.1145/3192366.3192406}
}
@inproceedings{vstte17io,
author = {Hugo Férée and Johannes Åman Pohjola and Ramana Kumar and Scott Owens and Magnus O. Myreen and Son Ho},
editor = {Ruzica Piskac and Philipp Rümmer},
title = {Program Verification in the Presence of {I/O}: Semantics, verified library routines, and verified applications},
booktitle = {Verified Software. Theories, Tools, and Experiments ({VSTTE})},
year = {2018},
series = {Lecture Notes in Computer Science},
volume = {11294},
publisher = {Springer},
url = {https://cakeml.org/vstte18.pdf},
doi = {10.1007/978-3-030-03592-1_6}
}
@inproceedings{vstte17votes,
author = {Milad Ketab Ghale and Dirk Pattinson and Ramana Kumar},
editor = {Ruzica Piskac and Philipp Rümmer},
title = {Verified Certificate Checking for Counting Votes},
booktitle = {Verified Software. Theories, Tools, and Experiments ({VSTTE})},
year = {2018},
series = {Lecture Notes in Computer Science},
volume = {11294},
publisher = {Springer},
url = {https://link.springer.com/chapter/10.1007/978-3-030-03592-1_5},
doi = {10.1007/978-3-030-03592-1_5}
}
@inproceedings{fmcad18,
author = {Heiko Becker and Nikita Zyuzin and Raphael Monat and Eva Darulova and Magnus O. Myreen and Anthony Fox},
title = {A Verified Certificate Checker for Finite-Precision Error Bounds in {Coq} and {HOL4}},
booktitle = {Formal Methods in Computer Aided Design ({FMCAD})},
year = {2018},
publisher = {{IEEE}},
url = {https://cakeml.org/fmcad18.pdf}
}
@article{oopsla20,
author = {Alejandro Gómez-Londoño and Johannes Åman Pohjola and Hira Taqdees Syeda and Magnus O. Myreen and Yong Kiam Tan},
title = {Do you have space for dessert? {A} verified space cost semantics for {CakeML} programs},
journal = {Proc. ACM Program. Lang. (OOPSLA)},
volume = {4},
pages = {204:1--204:29},
year = {2020},
url = {https://cakeml.org/oopsla20.pdf},
doi = {10.1145/3428272}
}
This file was generated by bibtex2html 1.99.