Magnus Myreen

Magnus Myreen (

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

May 2016ICFP'16 has accepted our latest paper on CakeML: A New Verified Compiler Backend for CakeML

Apr 2016 — Had the pleasure to visit Eva Darulova at MPI and learn about her impressive Rosa compiler.

Apr 2016 — Gave a talk at Philippa Gardner's Verified Trustworthy Software Systems, Specialist Meeting at Imperial College.

Mar 2016 — Recruiting a PhD student and a postdoc.

Jan 2016 — JAR has published our article Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation

Jan 2016 — I'll be involved in organising CADE-26 at Chalmers in 2017

Dec 2015 - Jan 2016 — Visited Gerwin Klein's group at NICTA / Data61.

Dec 2015 — ESOP'16 has accepted our paper on Functional Big-step Semantics

Aug 2015 — became Associate Professor at Chalmers CSE.

May 2015 — had the pleasure of visiting Edinburgh LFCS, gave a talk there.

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.