Magnus Myreen

Magnus Myreen (

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

Dec 2022 — My PhD student Oskar Abrahamsson successfully defended his PhD thesis on Candle.

Dec 2022 — I'm an examiner on Heiko Becker's PhD thesis on floating-point programs.

Aug 2022 — I will be on the programme committee of PLDI'23.

Aug 2022 — attended FLoC 2022 in Isreal, where many interesting papers were presented at ITP'22, e.g. this and this.

Apr 2022 — I had the pleasure of visiting Jeremy Avigad at CMU

Mar 2022 — ITP'22 has accepted our papers: Candle: A Verified Implementation of HOL Light and Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification

Feb 2022 — ECOOP'22 has accepted our paper on Verified Compilation and Optimization of Floating-Point Programs in CakeML

Sep 2021 — I took part in an in-person(!) Dagstuhl Seminar on Integrated Deduction

Sep 2021 — My PhD student Andreas Loow successfully defended his PhD thesis.

Jun 2021 — I gave a keynote presentation at ITP 2021.

Apr 2021 — I served on the grading committee at Arve Gengelbach's PhD defence at Uppsala University.

Dec 2020 — My paper on A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) has been accepted for CPP'21 and received a Distinguished Paper Award.

Sep 2020OOPSLA'20 has accepted our paper on a verified space cost semantics for CakeML programs

Aug 2020 — I'm organizing a series of online talks on CakeML and HOL.

Apr 2020 — Serving on the ICFP'20 programme committee

Feb 2020 — Serving on the PLDI'20 programme committee

Dec 2019 - Jan 2020 — Visited Trustworthy Systems at Data61/CSIRO in Sydney and Canberra, Australia

Aug 2019 — I gave lectures at Marktoberdorf summer school

Jun 2019 — ITP has accepted our paper on proofs about non-terminating programs

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

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

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

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

Jan 2019PLDI'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:

Previously in my group at Chalmers: