Magnus Myreen

Magnus.Myreen (@cl.cam.ac.uk)

Royal Society University Research Fellow, CL, Cambridge
but nowadays at Chalmers
Recent activity

May 2015 — gave a guest lecture on compiler verification at Josef Svenningsson's Masters course on Compiler Construction.

May 2015 — a beta version of the verified CakeML executable is available here.

May 2015ITP accepted a paper on which I am a co-author.

May 2015 — had the pleasure of visiting Edinburgh LFCS, gave a talk there.

Apr 2015 — taking part in a Dagstuhl seminar on Qualification of FM Tools by Darren Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels.

Feb 2015 — the Journal of Automated Reasoning (JAR) has accepted our paper on the Milawa/Jitawa work.



My research focuses on program verification, interactive theorem proving and, particularly, the challenges of making interactive proofs more automatic / scale to real code. This webpage provides a brief introduction to my research in the following areas:

  • Decompilation into logic — verification of machine code
  • Proof-producing synthesis from logic
  • Verified Lisp and ML runtimes
  • Connecting things up: verified stacks

Send me an email if you'd like to know more. My email address is at the top of the page.