Automatically Introducing Tail Recursion in CakeML. - Oskar Abrahamsson; Magnus O. Myreen (TFP, 2017)

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. - Son Ho; Oskar Abrahamsson; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan; Michael Norrish (IJCAR, 2018)

Verified compilation on a verified processor. - Andreas Lööw; Ramana Kumar; Yong Kiam Tan; Magnus O. Myreen; Michael Norrish; Oskar Abrahamsson; Anthony C. J. Fox (PLDI, 2019)

Proof-Producing Synthesis of CakeML from Monadic HOL Functions. - Oskar Abrahamsson; Son Ho; Hrutvik Kanabar; Ramana Kumar; Magnus O. Myreen; Michael Norrish; Yong Kiam Tan (J. Autom. Reason., 2020)

A verified proof checker for higher-order logic. - Oskar Abrahamsson (J. Log. Algebraic Methods Program., 2020)

Candle: A Verified Implementation of HOL Light. - Oskar Abrahamsson; Magnus O. Myreen; Ramana Kumar; Thomas Sewell (ITP, 2022)

Fast, Verified Computation for Candle. - Oskar Abrahamsson; Magnus O. Myreen (ITP, 2023)

PureCake: A Verified Compiler for a Lazy Functional Language. - Hrutvik Kanabar; Samuel Vivien; Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Johannes Åman Pohjola; Riccardo Zanetti (Proc. ACM Program. Lang., 2023)

Cakes That Bake Cakes: Dynamic Computation in CakeML. - Thomas Sewell; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar; Alexander Mihajlovic; Oskar Abrahamsson; Scott Owens (Proc. ACM Program. Lang., 2023)

Fast, Verified Computation for HOL ITPs. - Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Hrutvik Kanabar; Johannes Åman Pohjola (J. Autom. Reason., 2025)