Follow
Hrutvik Kanabar
Title
Cited by
Cited by
Year
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
132020
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
42023
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
42022
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
Verified efficient libraries for CakeML
H KANABAR
The system can't perform the operation now. Try again later.
Articles 1–7