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)

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. - Hrutvik Kanabar; Anthony C. J. Fox; Magnus O. Myreen (ITP, 2022)

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)

Verified Inlining and Specialisation for PureCake. - Hrutvik Kanabar; Kacper Korban; Magnus O. Myreen (ESOP (2), 2024)

A Graded Modal Approach to Relaxed Semantic Declassification. - Vineet Rajani; Alex Coleman; Hrutvik Kanabar (CSF, 2025)

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