Proof-producing synthesis of CakeML from monadic HOL functions O Abrahamsson, S Ho, H Kanabar, R Kumar, MO Myreen, M Norrish, ... Journal of Automated Reasoning 64, 1287-1306, 2020 | 15 | 2020 |
PureCake: A verified compiler for a lazy functional language H Kanabar, S Vivien, O Abrahamsson, MO Myreen, M Norrish, JÅ Pohjola, ... Proceedings of the ACM on Programming Languages 7 (PLDI), 952-976, 2023 | 5 | 2023 |
Taming an authoritative Armv8 ISA specification: L3 validation and CakeML compiler verification H Kanabar, ACJ Fox, MO Myreen 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022 | 4 | 2022 |
Verified Inlining and Specialisation for PureCake H Kanabar, K Korban, MO Myreen European Symposium on Programming, 275-301, 2024 | | 2024 |
Verified compilation of a purely functional language to a realistic machine semantics H Kanabar University of Kent,, 2024 | | 2024 |
Implementing and verifying a compiler optimisation for CakeML Computer Science Tripos–Part II King’s College May 18, 2018 H Kanabar | | 2018 |
PureCake: A Verified Compiler for a Lazy Functional H KANABAR, S VIVIEN, O ABRAHAMSSON, MO MYREEN, M NORRISH, ... | | |
Verified efficient libraries for CakeML H KANABAR | | |