Magnus O. Myreen

Registered user since Thu 20 Apr 2017

Name:Magnus O. Myreen
Bio:

I did a B.A. in Computer Science at the University of Oxford, tutored by Dr Jeff Sanders.

I completed my Ph.D. on program verification in 2009 at the University of Cambridge, supervised by Prof. Mike Gordon. My PhD dissertation was selected as the winner of the BCS Distinguished Dissertation Competition 2010.

In 2012, I became a Royal Society Research Fellow, UK.

In 2014, I moved to Chalmers where I became a tenured Associate Professor in 2015.

Affiliation:Chalmers University of Technology
Research interests:Formal verification, interactive theorem provers, compilers, machine code, functional programming

Contributions

CPP 2022 Committee Member in Steering Committee within the CPP 2022-track
PLDI 2021 Committee Member in Program Committee within the PLDI-track
CPP 2021 Author of A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) within the CPP 2021-track
Steering Committee Member in Steering Committee within the CPP 2021-track
REMS-DeepSpec 2020 Committee Member in Program Committee within the REMS-DeepSpec 2020-track
FormaliSE 2020 PC Member in Program Committee within the FormaliSE 2020-track
SPLASH 2020 Author of Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs within the OOPSLA Artifacts-track
Author of Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs within the OOPSLA-track
ICFP 2020 Committee Member in Program Committee within the ICFP Program-track
POPL 2020 Committee Member in Program Committee within the Research Papers-track
FormaliSE 2019 Author of A Proof-Producing Translator for Verilog Development in HOL within the FormaliSE 2019-track
CPP 2019 Program Co-Chair in Program Committee within the CPP 2019-track
Author of Business Meeting within the CPP 2019-track
Session Chair of Keynote 1 and Research Paper (part of CPP 2019)
DeepSpec 2018 Speaker of CakeML: from functions to machine code with proof all the way within the DeepSpec 2018-track
PLDI 2019 Committee Member in External Review Committee within the PLDI Research Papers-track
Author of Verified Compilation on a Verified Processor within the PLDI Research Papers-track
CPP 2018 Committee Member in Program Committee within the CPP 2018-track
PLDI 2018 Author of VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models within the PLDI Research Papers-track
ICFP 2017 Presenter of Tutorial T1: Writing Verified Programs in CakeML within the Tutorials-track
Author of Verifying Efficient Function Calls in CakeML within the Research Papers-track
Presenter of Tutorial T1: Writing Verified Programs in CakeML (part 2) within the Tutorials-track
Presenter of Tutorial T1: Writing Verified Programs in CakeML (part 3) within the Tutorials-track
CPP 2017 Author of Verified compilation of CakeML to multiple machine-code targets within the CPP-track
Scheme 2016 Author of A verified Lisp implementation for a verified theorem prover within the Scheme-track
PLDI 2017 Tutorial organizer of Writing Verified Programs in CakeML within the PLDI Tutorials-track
ICFP 2016 Author of A New Verified Compiler Backend for CakeML within the Research Papers-track