publications.bib

@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}
}
@inproceedings{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 = {http://www.cse.chalmers.se/~loow/papers/cpp2021.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.