Magnus O. Myreen

Available identifiers

zbMath Open myreen.magnus-oMaRDI QIDQ286789

List of research outcomes

Publication	Date of Publication	Type
Fast, verified computation for candle	2024-11-26	Paper
Candle: a verified implementation of HOL light	2024-07-15	Paper
Taming an authoritative armv8 ISA specification: L3 validation and cakeml compiler verification	2024-07-15	Paper
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
The Reflective Milawa Theorem Prover Is Sound	2014-09-08	Paper
HOL with Definitions: Semantics, Soundness, and a Verified Implementation	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

This page was built for person: Magnus O. Myreen