Folgen
Ramana Kumar
Titel
Zitiert von
Zitiert von
Jahr
CakeML: a verified implementation of ML
R Kumar, MO Myreen, M Norrish, S Owens
ACM SIGPLAN Notices 49 (1), 179-191, 2014
4932014
Functional big-step semantics
S Owens, MO Myreen, R Kumar, YK Tan
Programming Languages and Systems: 25th European Symposium on Programming …, 2016
1162016
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
1002016
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
902020
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
802021
The verified CakeML compiler backend
YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish
Journal of Functional Programming 29, e2, 2019
752019
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
632022
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
632016
TacticToe: learning to prove with tactics
T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish
Journal of Automated Reasoning 65, 257-286, 2021
62*2021
Verified characteristic formulae for CakeML
A Guéneau, MO Myreen, R Kumar, M Norrish
Programming Languages and Systems: 26th European Symposium on Programming …, 2017
552017
Penalizing side effects using stepwise relative reachability
V Krakovna, L Orseau, R Kumar, M Martic, S Legg
arXiv preprint arXiv:1806.01186, 2018
542018
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
402014
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
392019
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
362022
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
312018
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
302017
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
292017
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
282018
Modeling AGI safety frameworks with causal influence diagrams
T Everitt, R Kumar, V Krakovna, S Legg
arXiv preprint arXiv:1906.08663, 2019
232019
Steps towards verified implementations of HOL Light
MO Myreen, S Owens, R Kumar
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013
232013
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20