Front page
Research:
 • Decompilation
 • Synthesis
 • Lisp and ML
 • Verified stacks
Funding
Teaching
Biography
Committees etc.
Publications
Talks
Magnus Myreen

Magnus Myreen (myreen@chalmers.se)

Professor (in Swedish: bitr. prof.), CS, CSE, Chalmers (room 6478)
Recent activity

May 2025 — Three recently accepted papers: ITP 2025: GOL in GOL in HOL: Verified Circuits in Conway's Game of Life; CP 2025: Practically Feasible Proof Logging for Pseudo-Boolean Optimization; SAT 2025: Efficient Certified Reasoning for Binarized Neural Networks.

Jan 2025 — The Journal of Automated Reasoning has accepted our submission: Fast, Verified Computation for Candle and Automated Translation into Code Equations.

Jun 2024 — I'll give a keynote at PLDI 2024 on compiler verification.

May 2024 — Recently accepted: CAV 2024 paper and IJCAR 2024 paper.

Jan 2024 — Our 2014 paper CakeML: A Verified Implementation of ML has won the ACM SIGPLAN Most Influential POPL Paper Award.

Dec 2023 — The AAAI Conference on Artificial Intelligence (AAAI-24) has accepted our paper End-to-End Verification for Subgraph Solving.

Dec 2023 — ESOP 2024 has accepted our paper Verified inlining and specialisation for PureCake.

Nov 2023 — I became chair of the steering committee for the ITP conference series, when Lawrence Paulson stepped down.

Oct 2023 — Started a ten-month-long sabbatical at Cambridge UK, where I will work part-time for Arm Ltd.

Jun 2023 — I got promoted to professor. My promotion lecture was titled: Interactive Theorem Proving: History, Use, and Advancement.

Jun 2023 — I'll give at talk at NANDA 2023 in London 11-12 Sep.

Jun 2023 — My PhD student Alejandro Gomez successfully defended his PhD on Monday 12 June.

Jun 2023 — I'll be on the programme committee for CPP'24.

Apr 2023 — I'm an author on two PLDI 2023 papers: PureCake: A verified compiler for a lazy functional language and Cakes that bake cakes: Dynamic computation in CakeML

Apr 2023 — I've received an Amazon Research Award for my proposal Compiling Dafny to CakeML.

Apr 2023 — ITP'23 accepted our paper on Fast, Verified Computation for Candle.

Mar 2023 — I had the pleasure of visiting Clément Pit-Claudel and his new group at EPFL, and met many interesting people, including Viktor Kuncak, Martin Odersky and James Larus to name just a few.

Jan 2023 — I visited Ilya Sergey and his group at NUS.

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 — attended FLoC 2022 in Israel, where many interesting papers were presented at ITP'22, e.g. this and this.



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.

Previously in my group at Chalmers: