Magnus O. Myreen

Available identifiers

zbMath Open myreen.magnus-oMaRDI QIDQ286789

List of research outcomes

Publication	Date of Publication	Type
Icing: supporting fast-math style optimizations in a verified compiler	2024-02-16	Paper
https://portal.mardi4nfdi.de/entity/Q6157241	2023-06-20	Paper
Characteristic formulae for liveness properties of non-terminating CakeML programs	2023-02-03	Paper
Automatically Introducing Tail Recursion in CakeML	2022-12-09	Paper
\texttt{cake\_lpr}: verified propagation redundancy checking in CakeML	2021-10-18	Paper
Proof-producing synthesis of CakeML from monadic HOL functions	2020-11-02	Paper
The verified CakeML compiler backend	2019-11-22	Paper
A verified generational garbage collector for CakeML	2019-08-21	Paper
Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions	2018-10-18	Paper
Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)	2018-10-04	Paper
A verified generational garbage collector for CakeML	2018-01-04	Paper
Verified Characteristic Formulae for CakeML	2017-05-19	Paper
The reflective Milawa theorem prover is sound (down to the machine code that runs it)	2016-05-26	Paper
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation	2016-05-26	Paper
Pattern Matches in HOL:	2015-09-14	Paper
Verified just-in-time compiler on x86	2015-06-11	Paper
Transforming Programs into Recursive Functions	2015-03-19	Paper
HOL with Definitions: Semantics, Soundness, and a Verified Implementation	2014-09-08	Paper
The Reflective Milawa Theorem Prover Is Sound	2014-09-08	Paper
Proof-producing translation of higher-order logic into pure and stateful ML	2014-08-14	Paper
Proof-producing synthesis of ML from higher-order logic	2014-07-21	Paper
CakeML	2014-04-10	Paper
Steps towards Verified Implementations of HOL Light	2013-08-07	Paper
Function extraction	2012-07-20	Paper
A Verified Runtime for a Verified Theorem Prover	2011-08-17	Paper
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture	2010-09-14	Paper
Separation Logic Adapted for Proofs by Rewriting	2010-09-14	Paper
Hoare Logic for ARM Machine Code	2008-07-01	Paper
Hoare Logic for Realistically Modelled Machine Code	2007-09-03	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Magnus O. Myreen