Magnus Myreen (myreen@chalmers.se)
Professor (in Swedish:
bitr. prof. ),
CS ,
CSE ,
Chalmers (room 6478)
Recent activity
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 .
VIDEO
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:
