@article{DavisM15,
  author    = {Jared Davis and
               Magnus O. Myreen},
  title     = {The Reflective {Milawa} Theorem Prover is Sound 
               (Down to the Machine Code that Runs it)},
  journal   = {Journal of Automated Reasoning ({JAR})},
  publisher = {Springer},
  year      = {2015},
  issn      = {0168-7433},
}
@inproceedings{KumarMNO14,
  author    = {Ramana Kumar and
               Magnus O. Myreen and
               Michael Norrish and
               Scott Owens},
  title     = {{CakeML}: A verified implementation of {ML}},
  booktitle = {Principles of Programming Languages ({POPL})},
  publisher = {ACM},
  year      = {2014},
  pages     = {179--192},
}
@inproceedings{MyreenD14,
  author    = {Magnus O. Myreen and
               Jared Davis},
  editor    = {Gerwin Klein and
               Ruben Gamboa},
  title     = {The Reflective Milawa Theorem Prover Is Sound -
               (Down to the Machine Code That Runs It)},
  booktitle = {Interactive Theorem Proving ({ITP})},
  pages     = {421--436},
  publisher = {Springer},
  year      = {2014},
}
@inproceedings{KumarAMO14,
  author    = {Ramana Kumar and
               Rob Arthan and
               Magnus O. Myreen and
               Scott Owens},
  editor    = {Gerwin Klein and
               Ruben Gamboa},
  title     = {{HOL} with Definitions: Semantics, Soundness,
               and a Verified Implementation},
  booktitle = {Interactive Theorem Proving ({ITP})},
  pages     = {308--324},
  publisher = {Springer},
  year      = {2014},
}
@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},
  volume    = {24},
  pages     = {284--315},
  month     = {may},
  year      = {2014},
}
@inproceedings{SewellMK13,
  author    = {Thomas Arthur Leck Sewell and
               Magnus O. Myreen and
               Gerwin Klein},
  editor    = {Hans{-}Juergen Boehm and
               Cormac Flanagan},
  title     = {Translation validation for a verified {OS} kernel},
  booktitle = {Programming Language Design and Implementation ({PLDI})},
  pages     = {471--482},
  publisher = {{ACM}},
  year      = {2013},
}
@inproceedings{MyreenC13,
  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})},
  pages     = {66--81},
  editor    = {Georges Gonthier and
               Michael Norrish},
  publisher = {Springer},
  year      = {2013},
}
@inproceedings{MyreenOK13,
  author    = {Magnus O. Myreen and
               Scott Owens and
               Ramana Kumar},
  editor    = {Sandrine Blazy and
               Christine Paulin{-}Mohring and
               David Pichardie},
  title     = {Steps towards Verified Implementations of {HOL} Light},
  booktitle = {Interactive Theorem Proving ({ITP})},
  pages     = {490--495},
  publisher = {Springer},
  year      = {2013},
}
@inproceedings{MyreenO12,
  author    = {Magnus O. Myreen and
               Scott Owens},
  editor    = {Peter Thiemann and
               Robby Bruce Findler},
  title     = {Proof-producing synthesis of {ML} from higher-order logic},
  booktitle = {International Conference on Functional Programming ({ICFP})},
  pages     = {115--126},
  publisher = {{ACM}},
  year      = {2012},
}
@inproceedings{MyreenGS12,
  author    = {Magnus O. Myreen and
               Michael J. C. Gordon and
               Konrad Slind},
  title     = {Decompilation into logic - Improved},
  pages     = {78--81},
  editor    = {Gianpiero Cabodi and
               Satnam Singh},
  booktitle = {Formal Methods in Computer-Aided Design ({FMCAD})},
  publisher = {{IEEE}},
  year      = {2012},
}
@inproceedings{Myreen12,
  author    = {Magnus O. Myreen},
  title     = {Functional Programs: Conversions between Deep and Shallow Embeddings},
  pages     = {412--417},
  year      = {2012},
  editor    = {Lennart Beringer and
               Amy P. Felty},
  booktitle = {Interactive Theorem Proving ({ITP})},
  publisher = {Springer},
}
@article{MyreenG12,
  author    = {Magnus O. Myreen and
               Michael J. C. Gordon},
  title     = {Function extraction},
  journal   = {Sci. Comput. Program.},
  volume    = {77},
  number    = {4},
  pages     = {505--517},
  year      = {2012},
  publisher = {Elsevier},
}
@inproceedings{MyreenD11,
  author    = {Magnus O. Myreen and
               Jared Davis},
  title     = {A Verified Runtime for a Verified Theorem Prover},
  booktitle = {Interactive Theorem Proving ({ITP})},
  pages     = {265--280},
  year      = {2011},
  editor    = {Marko C. J. D. van Eekelen and
               Herman Geuvers and
               Julien Schmaltz and
               Freek Wiedijk},
}
@inproceedings{Myreen10vstte,
  author    = {Magnus O. Myreen},
  title     = {Reusable Verification of a Copying Collector},
  booktitle = {Verified Software: Theories, Tools, Experiments ({VSTTE})},
  pages     = {142--156},
  editor    = {Gary T. Leavens and
               Peter W. O'Hearn and
               Sriram K. Rajamani},
  publisher = {Springer},
  year      = {2010},
}
@article{SewellSOZM10,
  author    = {Peter Sewell and
               Susmit Sarkar and
               Scott Owens and
               Zappa Nardelli, Francesco and
               Magnus O. Myreen},
  title     = {{x86-TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors},
  journal   = {Communications of the ACM},
  volume    = {53},
  number    = {7},
  pages     = {89--97},
  month     = {jul},
  year      = {2010},
}
@inproceedings{FoxM10,
  author    = {Anthony C. J. Fox and
               Magnus O. Myreen},
  title     = {A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture},
  booktitle = {Interactive Theorem Proving ({ITP})},
  pages     = {243--258},
  editor    = {Matt Kaufmann and
               Lawrence C. Paulson},
  publisher = {Springer},
  year      = {2010},
}
@inproceedings{Myreen10itp,
  author    = {Magnus O. Myreen},
  title     = {Separation Logic Adapted for Proofs by Rewriting},
  booktitle = {Interactive Theorem Proving ({ITP})},
  pages     = {485--489},
  editor    = {Matt Kaufmann and
               Lawrence C. Paulson},
  publisher = {Springer},
  year      = {2010},
}
@inproceedings{Myreen10,
  author    = {Magnus O. Myreen},
  title     = {Verified just-in-time compiler on x86},
  booktitle = {Principles of Programming Languages ({POPL})},
  pages     = {107--118},
  editor    = {Manuel V. Hermenegildo and
               Jens Palsberg},
  publisher = {{ACM}},
  year      = {2010},
}
@incollection{FoxGM10,
  author    = {Anthony C. J. Fox and
               Michael J. C. Gordon and
               Magnus O. Myreen},
  booktitle = {Design and Verification of Microprocessor Systems
               for High-Assurance Applications},
  editor    = {David S. Hardin},
  title     = {Specification and Verification of ARM Hardware and Software},
  pages     = {221-247},
  publisher = {Springer},
  year      = {2010},
}
@inproceedings{MyreenG09,
  author    = {Magnus O. Myreen and
               Michael J. C. Gordon},
  title     = {Verified {LISP} Implementations on {ARM}, x86 and {PowerPC}},
  booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs})},
  pages     = {359--374},
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  publisher = {Springer},
  year      = {2009},
}
@inproceedings{MyreenSG09,
  author    = {Magnus O. Myreen and
               Konrad Slind and
               Michael J. C. Gordon},
  title     = {Extensible Proof-Producing Compilation},
  booktitle = {Compiler Construction ({CC})},
  pages     = {2--16},
  editor    = {Oege de Moor and
               Michael I. Schwartzbach},
  publisher = {Springer},
  year      = {2009},
}
@inproceedings{SarkarSNORBMA09,
  author    = {Susmit Sarkar and
               Peter Sewell and
               Zappa Nardelli, Francesco and
               Scott Owens and
               Tom Ridge and
               Thomas Braibant and
               Magnus O. Myreen and
               Jade Alglave},
  title     = {The semantics of {x86-CC} multiprocessor machine code},
  booktitle = {Principles of Programming Languages ({POPL})},
  pages     = {379--391},
  year      = {2009},
  editor    = {Zhong Shao and
               Benjamin C. Pierce},
  publisher = {{ACM}},
  year      = {2009},
}
@inproceedings{AlglaveFIMSSN09,
  author    = {Jade Alglave and
               Anthony C. J. Fox and
               Samin Ishtiaq and
               Magnus O. Myreen and
               Susmit Sarkar and
               Peter Sewell and
               Francesco Zappa Nardelli},
  title     = {The semantics of power and {ARM} multiprocessor machine code},
  booktitle = {Declarative Aspects of Multicore Programming ({DAMP})},
  pages     = {13--24},
  editor    = {Leaf Petersen and
               Manuel M. T. Chakravarty},
  publisher = {{ACM}},
  year      = {2009},
}
@article{MyreenG09x,
 author     = {Magnus O. Myreen and
               Michael J. C. Gordon},
 title      = {Transforming Programs into Recursive Functions},
 journal    = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {July, 2009},
 volume     = {240},
 year       = {2009},
 pages      = {185--200},
 publisher  = {Elsevier Science Publishers B. V.},
}
@PhdThesis{Myreen09,
  author = {Magnus O. Myreen},
  title  = {Formal verification of machine-code programs},
  year   = {2009},
  school = {University of Cambridge},
}
@inproceedings{MyreenGS08,
  author    = {Magnus O. Myreen and
               Michael J. C. Gordon and
               Konrad Slind},
  title     = {Machine-Code Verification for Multiple Architectures -
               An Application of Decompilation into Logic},
  booktitle = {Formal Methods in Computer-Aided Design ({FMCAD})},
  pages     = {1--8},
  editor    = {Alessandro Cimatti and
               Robert B. Jones},
  publisher = {{IEEE}},
  year      = {2008},
}
@inproceedings{MyreenG07,
  author    = {Magnus O. Myreen and
               Michael J. C. Gordon},
  title     = {Hoare Logic for Realistically Modelled Machine Code},
  booktitle = {Tools and Algorithms for the Construction and
               Analysis of Systems ({TACAS})},
  pages     = {568--582},
  year      = {2007},
  editor    = {Orna Grumberg and
               Michael Huth},
  publisher = {Springer},
}
@inproceedings{MyreenFG07,
  author    = {Magnus O. Myreen and
               Anthony C. J. Fox and
               Michael J. C. Gordon},
  title     = {Hoare Logic for {ARM} Machine Code},
  pages     = {272--286},
  editor    = {Farhad Arbab and
               Marjan Sirjani},
  booktitle = {Fundamentals of Software Engineering ({FSEN})},
  publisher = {Springer},
  year      = {2007},
}
@inproceedings{BackEM07,
  author    = {Ralph{-}Johan Back and
               Johannes Eriksson and
               Magnus Myreen},
  title     = {Testing and Verifying Invariant Based Programs in
               the {SOCOS} Environment},
  booktitle = {Tests and Proofs ({TAP})},
  publisher = {Springer},
  pages     = {61--78},
  year      = {2007},
  editor    = {Yuri Gurevich and
               Bertrand Meyer},
}
@inproceedings{BackM05,
  author    = {Ralph{-}Johan Back and
               Magnus Myreen},
  title     = {Tool Support for Invariant Based Programming},
  booktitle = {Asia-Pacific Software Engineering Conference ({APSEC})},
  pages     = {711--718},
  year      = {2005},
  publisher = {{IEEE} Computer Society},
}