Magnus Myreen

Magnus Myreen (

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

Sep 2018Tobias Nipkow is spending five weeks of his sabbatical at Chalmers

Sep 2018Thomas Sewell started as a new postdoc in my group

May 2018 — I'll be speaking at the DeepSpec workshop at PLDI'18

May 2018 — Took part in a Dagstuhl meeting on Secure Compilation

Mar 2018 — two CakeML papers were accepted for FLoC'18: one at IJCAR and a short paper at ITP

Feb 2018 — I'm an author on a PLDI'18 paper

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.