@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,
note = {To appear},
author = {Yong Kiam Tan and Jiong Yang and Mate Soos and Magnus O. Myreen and Kuldeep S. Meel},
title = {Formally Certified Approximate Model Counting},
year = {2024},
booktitle = {Computer Aided Verification ({CAV})},
publisher = {Springer},
series = {Lecture Notes in Computer Science}
}
@inproceedings{IJCAR24,
note = {To appear},
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}
}
@inproceedings{ESOP24,
note = {To appear},
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{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.