Ramana Kumar
Titre
Citée par
Citée par
Année
CakeML: a verified implementation of ML
R Kumar, MO Myreen, M Norrish, S Owens
ACM SIGPLAN Notices 49 (1), 179-191, 2014
3142014
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
802016
Functional big-step semantics
S Owens, MO Myreen, R Kumar, YK Tan
European Symposium on Programming, 589-615, 2016
792016
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
68*2014
Self-formalisation of higher-order logic
R Kumar, R Arthan, MO Myreen, S Owens
Journal of Automated Reasoning 56 (3), 221-259, 2016
542016
The verified CakeML compiler backend
YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish
Journal of Functional Programming 29, 2019
352019
Verified characteristic formulae for CakeML
A Guéneau, MO Myreen, R Kumar, M Norrish
European Symposium on Programming, 584-610, 2017
322017
Penalizing side effects using stepwise relative reachability
V Krakovna, L Orseau, R Kumar, M Martic, S Legg
arXiv preprint arXiv:1806.01186, 2018
242018
Steps towards verified implementations of HOL Light
MO Myreen, S Owens, R Kumar
International Conference on Interactive Theorem Proving, 490-495, 2013
212013
Learning to prove with tactics
T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish
arXiv preprint arXiv:1804.00596, 2018
19*2018
A proof strategy language and proof script generation for Isabelle/HOL
Y Nagashima, R Kumar
International Conference on Automated Deduction, 528-545, 2017
192017
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
172018
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
172018
(Nominal) unification by recursive descent with triangular substitutions
R Kumar, M Norrish
International Conference on Interactive Theorem Proving, 51-66, 2010
152010
Reward tampering problems and solutions in reinforcement learning: A causal influence diagram perspective
T Everitt, M Hutter, R Kumar, V Krakovna
Synthese, 1-33, 2021
142021
Self-compilation and self-verification
R Kumar
University of Cambridge, Computer Laboratory, 2016
142016
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
132019
Proof-producing reflection for HOL
B Fallenstein, R Kumar
International Conference on Interactive Theorem Proving, 170-186, 2015
132015
Modeling AGI safety frameworks with causal influence diagrams
T Everitt, R Kumar, V Krakovna, S Legg
arXiv preprint arXiv:1906.08663, 2019
112019
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
112017
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20