@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.},
}
@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},
}