Magnus Myreen

Magnus Myreen (

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

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

Jun 2017 — Our paper on Verifying Efficient Function Calls in CakeML will appear at ICFP'17.

Jun 2017 — Our paper on A Verified Generational Garbage Collector for CakeML will appear at ITP'17.

Jun 2017 — My MSc student Oskar Abrahamsson and my BSc students Rikard Hjort, Jakob Holmgren and Christian Persson presented their work at TFP'17.

Mar 2017 — I will be on the programme committee of CPP 2017.

Dec 2016 — I will be hiring PhD students in 2017, thanks to a generous grant from SSF.

Dec 2016ESOP'17 has accepted our paper on Verified Characteristic Formulae for CakeML.

Nov 2016CPP'17 accepted our paper on target-specific aspects of the CakeML compiler.

Nov 2016 — Johannes Åman Pohjola started as a new postdoc.

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.