Ramana Kumar
Cited by
Cited by
CakeML: a verified implementation of ML
R Kumar, MO Myreen, M Norrish, S Owens
ACM SIGPLAN Notices 49 (1), 179-191, 2014
Functional big-step semantics
S Owens, MO Myreen, R Kumar, YK Tan
Programming Languages and Systems: 25th European Symposium on Programming …, 2016
Solving math word problems with process-and outcome-based feedback
J Uesato, N Kushman, R Kumar, F Song, N Siegel, L Wang, A Creswell, ...
arXiv preprint arXiv:2211.14275, 2022
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
Specification gaming: the flip side of AI ingenuity
V Krakovna, J Uesato, V Mikulik, M Rahtz, T Everitt, R Kumar, Z Kenton, ...
DeepMind Blog 3, 2020
Reward tampering problems and solutions in reinforcement learning: A causal influence diagram perspective
T Everitt, M Hutter, R Kumar, V Krakovna
Synthese 198 (Suppl 27), 6435-6467, 2021
The verified CakeML compiler backend
YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish
Journal of Functional Programming 29, e2, 2019
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
Self-formalisation of higher-order logic: Semantics, soundness, and a verified implementation
R Kumar, R Arthan, MO Myreen, S Owens
Journal of Automated Reasoning 56, 221-259, 2016
Verified characteristic formulae for CakeML
A Guéneau, MO Myreen, R Kumar, M Norrish
Programming Languages and Systems: 26th European Symposium on Programming …, 2017
Penalizing side effects using stepwise relative reachability
V Krakovna, L Orseau, R Kumar, M Martic, S Legg
arXiv preprint arXiv:1806.01186, 2018
Goal misgeneralization: Why correct specifications aren't enough for correct goals
R Shah, V Varma, R Kumar, M Phuong, V Krakovna, J Uesato, Z Kenton
arXiv preprint arXiv:2210.01790, 2022
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
HOL with definitions: Semantics, soundness, and a verified implementation
R Kumar, R Arthan, MO Myreen, S Owens
Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014
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
Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as …, 2018
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
Explaining grokking through circuit efficiency
V Varma, R Shah, Z Kenton, J Kramár, R Kumar
arXiv preprint arXiv:2309.02390, 2023
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB: (Short Paper)
R Kumar, E Mullen, Z Tatlock, MO Myreen
Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018
A proof strategy language and proof script generation for Isabelle/HOL
Y Nagashima, R Kumar
Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017
Modeling AGI safety frameworks with causal influence diagrams
T Everitt, R Kumar, V Krakovna, S Legg
arXiv preprint arXiv:1906.08663, 2019
The system can't perform the operation now. Try again later.
Articles 1–20