Magnus Myreen
Recent activity

Jan 2014 — co-author on two submissions to ITP'14: HOL with Definitions: Semantics, Soundness, and a Verified Implementation and The reflective Milawa theorem prover is sound (down to the machine code that runs it).

Oct 2013 — lecturing a new course on formal methods and functional programming.

Aug 2013CPP'13 has accepted my paper on a verified bignum arithmetic library.

Apr 2013 — I've been invited to give a tutorial at LOLA'13.

Mar 2013ITP'13 has accepted our paper on Steps Towards Verified Implementations of HOL Light, co-authors: Scott Owens and Ramana Kumar.

Feb 2013PLDI'13 has accepted a paper describing my collaboration with the L4.verified project, co-authors: Thomas Sewell and Gerwin Klein.

Dec 2012 — had the pleasure of meeting Carroll Morgan, author of one of my favourite books on program construction: Programming from Specifications.



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.