Magnus O. Myreen

According to our database1, Magnus O. Myreen authored at least 53 papers between 2005 and 2021.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2021
A minimalistic verified bootstrapped compiler (proof pearl).
Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020
Do you have space for dessert? a verified space cost semantics for CakeML programs.
Proc. ACM Program. Lang., 2020

Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason., 2020

2019
The verified CakeML compiler backend.
J. Funct. Program., 2019

A Verified Generational Garbage Collector for CakeML.
J. Autom. Reason., 2019

Verified compilation on a verified processor.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

A proof-producing translator for verilog development in HOL.
Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, 2019

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Clocked Definitions in HOL.
CoRR, 2018

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

VeriPhy: verified controller executables from verified cyber-physical system models.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
Verifying efficient function calls in CakeML.
Proc. ACM Program. Lang., 2017

A Verified Certificate Checker for Floating-Point Error Bounds.
CoRR, 2017

Automatically Introducing Tail Recursion in CakeML.
Proceedings of the Trends in Functional Programming - 18th International Symposium, 2017

Verified Characteristic Formulae for CakeML.
Proceedings of the Programming Languages and Systems, 2017

Verified compilation of CakeML to multiple machine-code targets.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation.
J. Autom. Reason., 2016

A new verified compiler backend for CakeML.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Functional Big-Step Semantics.
Proceedings of the Programming Languages and Systems, 2016

2015
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it).
J. Autom. Reason., 2015

Pattern Matches in HOL: - A New Representation and Improved Code Generation.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014
Proof-producing translation of higher-order logic into pure and stateful ML.
J. Funct. Program., 2014

CakeML: a verified implementation of ML.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

HOL with Definitions: Semantics, Soundness, and a Verified Implementation.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
Translation validation for a verified OS kernel.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Steps towards Verified Implementations of HOL Light.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012
Function extraction.
Sci. Comput. Program., 2012

Functional Programs: Conversions between Deep and Shallow Embeddings.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Proof-producing synthesis of ML from higher-order logic.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

Decompilation into logic - Improved.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011
A Verified Runtime for a Verified Theorem Prover.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors.
Commun. ACM, 2010

Reusable Verification of a Copying Collector.
Proceedings of the Verified Software: Theories, 2010

Verified just-in-time compiler on x86.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Separation Logic Adapted for Proofs by Rewriting.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Specification and Verification of ARM Hardware and Software.
Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009
Formal verification of machine-code programs.
PhD thesis, 2009

Transforming Programs into Recursive Functions.
Electron. Notes Theor. Comput. Sci., 2009

Verified LISP Implementations on ARM, x86 and PowerPC.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

The semantics of x86-CC multiprocessor machine code.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

The semantics of power and ARM multiprocessor machine code.
Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, 2009

Extensible Proof-Producing Compilation.
Proceedings of the Compiler Construction, 18th International Conference, 2009

2008
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic.
Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007
Testing and Verifying Invariant Based Programs in the SOCOS Environment.
Proceedings of the Tests and Proofs - 1st International Conference, 2007

Hoare Logic for Realistically Modelled Machine Code.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Hoare Logic for ARM Machine Code.
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

2005
Tool Support for Invariant Based Programming.
Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005


  Loading...