| CakeML: a verified implementation of ML R Kumar, MO Myreen, M Norrish, S Owens ACM SIGPLAN Notices 49 (1), 179-191, 2014 | 369 | 2014 |
| Functional big-step semantics S Owens, MO Myreen, R Kumar, YK Tan European Symposium on Programming, 589-615, 2016 | 90 | 2016 |
| A new verified compiler backend for CakeML YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016 | 86 | 2016 |
| Self-formalisation of higher-order logic R Kumar, R Arthan, MO Myreen, S Owens Journal of Automated Reasoning 56 (3), 221-259, 2016 | 57 | 2016 |
| The verified CakeML compiler backend YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Journal of Functional Programming 29, 2019 | 44 | 2019 |
| HOL with definitions: Semantics, soundness, and a verified implementation R Kumar, R Arthan, MO Myreen, S Owens International Conference on Interactive Theorem Proving, 308-324, 2014 | 39 | 2014 |
| Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish European Symposium on Programming, 584-610, 2017 | 34 | 2017 |
| Reward tampering problems and solutions in reinforcement learning: A causal influence diagram perspective T Everitt, M Hutter, R Kumar, V Krakovna Synthese 198 (27), 6435-6467, 2021 | 33 | 2021 |
| Penalizing side effects using stepwise relative reachability V Krakovna, L Orseau, R Kumar, M Martic, S Legg arXiv preprint arXiv:1806.01186, 2018 | 33 | 2018 |
| TacticToe: learning to prove with tactics T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish Journal of Automated Reasoning 65 (2), 257-286, 2021 | 31* | 2021 |
| A proof strategy language and proof script generation for Isabelle/HOL Y Nagashima, R Kumar International Conference on Automated Deduction, 528-545, 2017 | 24 | 2017 |
| Steps towards verified implementations of HOL Light MO Myreen, S Owens, R Kumar International Conference on Interactive Theorem Proving, 490-495, 2013 | 23 | 2013 |
| Software verification with ITPs should use binary code extraction to reduce the TCB R Kumar, E Mullen, Z Tatlock, MO Myreen International Conference on Interactive Theorem Proving, 362-369, 2018 | 22 | 2018 |
| Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions S Ho, O Abrahamsson, R Kumar, MO Myreen, YK Tan, M Norrish International Joint Conference on Automated Reasoning, 646-662, 2018 | 21 | 2018 |
| Modeling AGI safety frameworks with causal influence diagrams T Everitt, R Kumar, V Krakovna, S Legg arXiv preprint arXiv:1906.08663, 2019 | 20 | 2019 |
| Verified compilation on a verified processor A Lööw, R Kumar, YK Tan, MO Myreen, M Norrish, O Abrahamsson, A Fox Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019 | 19 | 2019 |
| (Nominal) unification by recursive descent with triangular substitutions R Kumar, M Norrish International Conference on Interactive Theorem Proving, 51-66, 2010 | 18 | 2010 |
| Verified compilation of CakeML to multiple machine-code targets A Fox, MO Myreen, YK Tan, R Kumar Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 17 | 2017 |
| Verifying efficient function calls in CakeML S Owens, M Norrish, R Kumar, MO Myreen, YK Tan Proceedings of the ACM on Programming Languages 1 (ICFP), 1-27, 2017 | 14 | 2017 |
| Self-compilation and self-verification R Kumar University of Cambridge, Computer Laboratory, 2016 | 14 | 2016 |
Magnus MyreenChalmers University of TechnologyVerified email at cl.cam.ac.uk
