Publications
2017
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan.
Verifying Efficient Function Calls in CakeML.
In International Conference on Functional Programming (ICFP), 2017.
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola:
A Verified Generational Garbage Collector for CakeML.
In Interactive Theorem Proving (ITP), 2017.
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish.
Verified Characteristic Formulae for CakeML.
In European Symposium on Programming (ESOP), 2017.
Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar.
Verified Compilation of CakeML to Multiple Machine-Code Targets.
In Certified Programs and Proofs (CPP), 2017.
2016
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish.
A New Verified Compiler Backend for CakeML.
In International Conference on Functional Programming (ICFP), 2016.
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens.
Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation.
In the Journal of Automated Reasoning (JAR), 2016.
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan.
Functional Big-step Semantics.
In European Symposium on Programming (ESOP), 2016.
2015
Thomas Tuerk, Magnus O. Myreen, Ramana Kumar.
Pattern Matches in HOL: A New Representation and Improved Code Generation.
In Interactive Theorem Proving (ITP), 2015.
Jared Davis, Magnus O. Myreen.
The self-verifying Milawa theorem prover is sound (down to the machine code that runs it).
In the Journal of Automated Reasoning (JAR), 2015. (Copyright Springer, official version)
bibtex
2014
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens.
CakeML: A Verified Implementation of ML.
In Principles of Programming Languages (POPL), 2014.
bibtex
Magnus O. Myreen, Jared Davis.
The reflective Milawa theorem prover is sound (down to the machine code that runs it).
In Interactive Theorem Proving (ITP), 2014.
bibtex
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens.
HOL with Definitions: Semantics, Soundness, and a Verified Implementation.
In Interactive Theorem Proving (ITP), 2014.
bibtex
Magnus O. Myreen, Scott Owens.
Proof-producing translation of higher-order logic into pure and stateful ML.
In Journal of Functional Programming (JFP), Volume 24, Issue 2–3, 2014. (Copyright Cambridge University Press, definitive version)
bibtex
2013
Thomas Sewell, Magnus O. Myreen and Gerwin Klein.
Translation validation for a verified OS kernel.
In Programming Language Design and Implementation (PLDI), 2013.
bibtex
Magnus O. Myreen and Gregorio Curello.
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code.
In Certified Programs and Proofs (CPP), 2013.
bibtex
Magnus O. Myreen, Scott Owens and Ramana Kumar.
Steps towards verified implementations of HOL Light.
In Interactive Theorem Proving (ITP), 2013.
bibtex
2012
Magnus O. Myreen and Scott Owens.
Proof-producing synthesis of ML from higher-order logic.
In International Conference on Functional Programming (ICFP), 2012.
bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon.
Decompilation into Logic — Improved.
In Formal Methods in Computer-Aided Design (FMCAD), 2012.
bibtex
Magnus O. Myreen.
Functional programs: conversions between deep and shallow embeddings.
In Interactive Theorem Proving (ITP), 2012.
bibtex
Magnus O. Myreen and Michael J. C. Gordon.
Function Extraction.
In Science of Computer Programming, 2010.
bibtex
2011
Magnus O. Myreen and Jared Davis.
A verified runtime for a verified theorem prover.
In Interactive Theorem Proving (ITP), 2011.
bibtex
2010
Magnus O. Myreen.
Reusable verification of a copying collector.
In Verified Software: Theories, Tools and Experiments (VSTTE), 2010.
bibtex
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli and Magnus O. Myreen.
x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors.
In Comm. ACM, 53(7), July 2010.
bibtex
Anthony Fox and Magnus O. Myreen.
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.
In Interactive Theorem Proving (ITP), 2010.
bibtex
Magnus O. Myreen.
Separation logic adapted for proofs by rewriting.
In Interactive Theorem Proving (ITP), 2010.
bibtex
Magnus O. Myreen.
Verified just-in-time compiler on x86.
In Principles of Programming Languages (POPL), 2010.
bibtex
Anthony C. J. Fox, Michael J. C. Gordon, and Magnus O. Myreen.
Specification and verification of ARM hardware and software.
In David S. Hardin, editor, Design and Verification of Microprocessor Systems
for High-Assurance Applications, Springer, 2010.
bibtex
2009
Magnus O. Myreen and Michael J. C. Gordon.
Verified LISP implementations on ARM, x86 and PowerPC.
In Theorem Proving in Higher-Order Logics (TPHOLs), 2009.
bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon.
Extensible proof-producing compilation.
In Compiler Construction (CC), 2009.
bibtex
Susmit Sarkar,
Peter Sewell,
Francesco Zappa Nardelli,
Scott Owens,
Tom Ridge,
Thomas Braibant,
Magnus O. Myreen,
Jade Alglave.
The Semantics of x86-CC Multiprocessor Machine Code.
In Principles of Programming Languages (POPL), 2009.
bibtex
Jade Alglave,
Anthony C. J. Fox,
Samin Ishtiaq,
Magnus O. Myreen,
Susmit Sarkar,
Peter Sewell,
Francesco Zappa Nardelli.
The semantics of Power and ARM multiprocessor machine code.
In Declarative aspects of multicore programming (DAMP), 2009.
bibtex
Magnus O. Myreen and Michael J. C. Gordon.
Transforming Programs into Recursive Functions.
In Electron. Notes Theor. Comput. Sci., 2009.
bibtex
2008
Magnus O. Myreen.
Formal verification of machine-code programs.
PhD dissertation, University of Cambridge, 2008.
bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon.
Machine-code verification for multiple architectures –
An application of decompilation into logic.
In Formal Methods in Computer-Aided Design (FMCAD), 2008.
bibtex
2007
Magnus O. Myreen and Michael J. C. Gordon.
Hoare Logic for Realistically Modelled Machine Code.
In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
bibtex
Magnus O. Myreen, Anthony C. J. Fox and Michael J. C. Gordon.
Hoare Logic for ARM Machine Code.
In Fundamentals of Software Engineering (FSEN), 2007.
bibtex
Ralph-Johan Back, Johannes Eriksson and Magnus Myreen.
Testing and Verifying Invariant Based Programs in the SOCOS Environment.
In Tests And Proofs (TAP), 2007.
bibtex
2005
Ralph-Johan Back and Magnus Myreen.
Tool Support for Invariant Based Programming.
In Asia-Pacific Software Engineering Conference (APSEC), 2005.
bibtex