## Publications

### 2018

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer.
VeriPhy: Verified Controller Executables from
Verified Cyber-Physical System Models.
In Programming Language Design and Implementation (PLDI), 2018.

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*. To apepar in International Joint Conference on Automated Reasoning (IJCAR), 2018.
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)*. To apepar in Interactive Theorem Proving (ITP), 2018.
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony Fox.

*A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4*. In Formal Methods in Computer-Aided Design (FMCAD), 2018.### 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.

Oskar Abrahamsson, Magnus O. Myreen.

*Automatically Introducing Tail Recursion in CakeML*. In Trends in Functional Programming (TFP), 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