BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Denmark
1 × Portugal
1 × Spain
1 × United Kingdom
3 × USA
Collaborated with:
S.Owens R.Kumar M.J.C.Gordon M.Norrish Y.K.Tan T.A.L.Sewell G.Klein K.Slind O.Abrahamsson A.Guéneau H.Becker E.Darulova Z.Tatlock B.Bohrer S.Mitsch A.Platzer S.Ho Andreas Lööw Anthony C. J. Fox S.Sarkar P.Sewell F.Z.Nardelli T.Ridge T.Braibant J.Alglave
Talks about:
verifi (9) ml (5) compil (4) produc (3) proof (3) cake (3) synthesi (2) function (2) semant (2) machin (2)

Person: Magnus O. Myreen

DBLP DBLP: Myreen:Magnus_O=

Contributed to:

POPL 20142014
PLDI 20132013
ICFP 20122012
POPL 20102010
CC 20092009
POPL 20092009
TACAS 20072007
ESOP 20162016
ESOP 20172017
IJCAR 20182018
CAV (2) 20192019
PLDI 20182018
PLDI 20192019

Wrote 13 papers:

POPL-2014-KumarMNO #implementation #ml #named
CakeML: a verified implementation of ML (RK, MOM, MN, SO), pp. 179–192.
PLDI-2013-SewellMK #kernel #validation
Translation validation for a verified OS kernel (TALS, MOM, GK), pp. 471–482.
ICFP-2012-MyreenO #higher-order #logic #ml #synthesis
Proof-producing synthesis of ML from higher-order logic (MOM, SO), pp. 115–126.
POPL-2010-Myreen #compilation
Verified just-in-time compiler on x86 (MOM), pp. 107–118.
CC-2009-MyreenSG #compilation
Extensible Proof-Producing Compilation (MOM, KS, MJCG), pp. 2–16.
POPL-2009-SarkarSNORBMA #multi #semantics
The semantics of x86-CC multiprocessor machine code (SS, PS, FZN, SO, TR, TB, MOM, JA), pp. 379–391.
TACAS-2007-MyreenG #hoare #logic
Hoare Logic for Realistically Modelled Machine Code (MOM, MJCG), pp. 568–582.
ESOP-2016-OwensMKT #functional #semantics
Functional Big-Step Semantics (SO, MOM, RK, YKT), pp. 589–615.
Verified Characteristic Formulae for CakeML (AG, MOM, RK, MN), pp. 584–610.
IJCAR-2018-HoAKMTN #monad #synthesis
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (SH, OA, RK, MOM, YKT, MN), pp. 646–662.
CAV-2019-BeckerDMT #compilation #named #optimisation
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler (HB, ED, MOM, ZT), pp. 155–173.
PLDI-2018-BohrerTMMP #bytecode #cyber-physical #modelling #named
VeriPhy: verified controller executables from verified cyber-physical system models (BB, YKT, SM, MOM, AP), pp. 617–630.
PLDI-2019-LoowKTMNAF #compilation
Verified compilation on a verified processor (AL, RK, YKT, MOM, MN, OA, ACJF), pp. 1041–1053.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.