Magnus Myreen

Magnus Myreen (

Associate Professor, CSE, Chalmers, D&IT room 5452
Recent activity

Feb 2018Lars Hupel is visiting for a week and talking about A Verified Compiler from Isabelle/HOL to CakeML

Feb 2018Assia Mahboubi and I will co-chair CPP 2019 — The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Jan 2018 — I gave an invited talk at ENTROPY'18

Dec-Jan 2017-2018 — Visited Trustworthy Systems at CSIRO Data61 again.

Aug 2017 — I was taken aback by the sudden and all too early death of my PhD supervisor, mentor and friend Prof Mike Gordon FRS.

Aug 2017 — I gave a series of 4 lectures at Marktoberdorf Summer School on the topic of compiler verification. My slides: lec-1, lec-2, lec-3, lec-4.

Jun 2017 — I'm very happy to hear that Ramana Kumar's PhD thesis received the John C. Reynolds Doctoral Dissertation Award 2017.

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:

My most recent work has focused on CakeML, which is an ML-style language with a formal semantics and a growing ecosystem of proofs and tools that support construction of verified applications. As far as I know, the CakeML compiler is the first verified compiler to have been bootstrapped.

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