Magnus Myreen

Magnus.Myreen (

former Royal Society University Research Fellow, CL, Cambridge
but nowadays at Chalmers
Recent activity

My recent activity is listed
on my Chalmers page.

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.