Magnus Myreen

Magnus Myreen (

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

May 2018 — I'm organising this year's CakeML Developers Meeting

Apr 2018 — I'll serve as external examiner for Lars Hupel's PhD

Mar 2018 — I'll give a keynote presentation at HCSS in May

Feb 2018 — I will again be lecturing at Marktoberdorf summer school

Feb 2018 — I acted as external examiner for Alastair Reid's PhD examination at Glasgow University

Jan 2018 — I'm looking to hire a new postdoc, deadline 28 Feb 2019

Jan 2018PLDI'19 accepted my PhD student's paper Verified Compilation on Verified Hardware

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:

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.

Below is a popular science video about my research. The video was made by Swedish Foundation for Strategic Research.

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

My group at Chalmers consists of:

  • Andreas Loow — PhD student started Sept 2016
  • Oskar Abrahamsson — PhD student started Aug 2017
  • Alejandro Gomez — PhD student started Sept 2017
  • Thomas Sewell — postdoc started Sept 2018
Previously in my group at Chalmers:
  • Johannes Aman Pohjola — postdoc Nov 2016 – Mar 2018