Magnus Myreen

Magnus Myreen (

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

Mar 2017I'm hiring two PhD students, applications are submitted here; I'm more than happy to answer questions about these positions.

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.

Oct 2016 — I served on the PhD committee for Jiaqi Tan's PhD thesis defence at CMU, USA.

Oct 2016 — I served on the PhD grading committee for Oliver Schwarz' PhD thesis defence at KTH, Sweden.

Sep 2016 — I've been invited to give a series of lectures at the Marktoberdorf Summer School in 2017.

Sep 2016 — Andreas Lööw starts as PhD student.

Sep 2016 — I've been invited to participate as a guest at the IFIP Working Group 2.8 - Functional Programming in Jun 2017.

Aug 2016 — I give talk on CakeML during a visit to Cambridge.

Aug 2016 — I'll give an invited talk at this year's Scheme Workshop, co-located with ICFP'16

Aug 2016 — Armaël Guéneau's 5-month visit comes to a close and CakeML now has an impressive formalisation of Arthur Charguéraud's characteristic formulas!

May 2016ICFP'16 has accepted our lates t 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.

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

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.