Ramana Kumar

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 37

Top Topics

Datalog Queries

Resource Bounded

Top Venues

J. Autom. Reason.

Publications

Zachary Kenton, Ramana Kumar, Sebastian Farquhar, Jonathan Richens, Matt MacDermott, Tom Everitt
Discovering Agents (Abstract Reprint). AAAI (2024)
Mary Phuong, Matthew Aitchison, Elliot Catt, Sarah Cogan, Alexandre Kaskasoli, Victoria Krakovna, David Lindner, Matthew Rahtz, Yannis Assael, Sarah Hodkinson, Heidi Howard, Tom Lieberum, Ramana Kumar, Maria Abi Raad, Albert Webson, Lewis Ho, Sharon Lin, Sebastian Farquhar, Marcus Hutter, Grégoire Delétang, Anian Ruoss, Seliem El-Sayed, Sasha Brown, Anca D. Dragan, Rohin Shah, Allan Dafoe, Toby Shevlane
Evaluating Frontier Models for Dangerous Capabilities. CoRR (2024)
Akhil Bagaria, Ray Jiang, Ramana Kumar, Tom Schaul
Scaling Goal-based Exploration via Pruning Proto-goals. CoRR (2023)
Vikrant Varma, Rohin Shah, Zachary Kenton, János Kramár, Ramana Kumar
Explaining grokking through circuit efficiency. CoRR (2023)
Zachary Kenton, Ramana Kumar, Sebastian Farquhar, Jonathan Richens, Matt MacDermott, Tom Everitt
Discovering agents. Artif. Intell. 322 (2023)
Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens
Cakes That Bake Cakes: Dynamic Computation in CakeML. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP (2022)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Zachary Kenton, Ramana Kumar, Sebastian Farquhar, Jonathan Richens, Matt MacDermott, Tom Everitt
Discovering Agents. CoRR (2022)
Jonathan Uesato, Nate Kushman, Ramana Kumar, H. Francis Song, Noah Y. Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, Irina Higgins
Solving math word problems with process- and outcome-based feedback. CoRR (2022)
Rohin Shah, Vikrant Varma, Ramana Kumar, Mary Phuong, Victoria Krakovna, Jonathan Uesato, Zac Kenton
Goal Misgeneralization: Why Correct Specifications Aren't Enough For Correct Goals. CoRR (2022)
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
Candle: A Verified Implementation of HOL Light. ITP (2022)
Matthew Rahtz, Vikrant Varma, Ramana Kumar, Zachary Kenton, Shane Legg, Jan Leike
Safe Deep RL in 3D Environments using Human Feedback. CoRR (2022)
Tom Everitt, Marcus Hutter, Ramana Kumar, Victoria Krakovna
Reward tampering problems and solutions in reinforcement learning: a causal influence diagram perspective. Synth. 198 (27) (2021)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65 (2) (2021)
Gopal Sarma, James Koppel, Gregory Malecha, Patrick Schultz, Eric Drexler, Ramana Kumar, Cody Roux, Philip Zucker
Formal Methods for the Informal Engineer: Workshop Recommendations. CoRR (2021)
Ramana Kumar, Jonathan Uesato, Richard Ngo, Tom Everitt, Victoria Krakovna, Shane Legg
REALab: An Embedded Perspective on Tampering. CoRR (2020)
Jonathan Uesato, Ramana Kumar, Victoria Krakovna, Tom Everitt, Richard Ngo, Shane Legg
Avoiding Tampering Incentives in Deep RL via Decoupled Approval. CoRR (2020)
Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan
Proof-Producing Synthesis of CakeML from Monadic HOL Functions. J. Autom. Reason. 64 (7) (2020)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
The verified CakeML compiler backend. J. Funct. Program. 29 (2019)
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox
Verified compilation on a verified processor. PLDI (2019)
Tom Everitt, Ramana Kumar, Victoria Krakovna, Shane Legg
Modeling AGI Safety Frameworks with Causal Influence Diagrams. CoRR (2019)
Tom Everitt, Ramana Kumar, Victoria Krakovna, Shane Legg
Modeling AGI Safety Frameworks with Causal Influence Diagrams. AISafety@IJCAI (2019)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
Learning to Prove with Tactics. CoRR (2018)
Ramana Kumar, Magnus O. Myreen
Clocked Definitions in HOL. CoRR (2018)
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. IJCAR (2018)
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. VSTTE (2018)
Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish
Verified Certificate Checking for Counting Votes. VSTTE (2018)
Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). ITP (2018)
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish
Verified Characteristic Formulae for CakeML. ESOP (2017)
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar
Verified compilation of CakeML to multiple machine-code targets. CPP (2017)
Yutaka Nagashima, Ramana Kumar
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. CADE (2017)
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
Verifying efficient function calls in CakeML. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
A new verified compiler backend for CakeML. ICFP (2016)
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. J. Autom. Reason. 56 (3) (2016)
Yutaka Nagashima, Ramana Kumar
A Proof Strategy Language and Proof Script Generation for Isabelle. CoRR (2016)
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan
Functional Big-Step Semantics. ESOP (2016)
Yong Kiam Tan, Scott Owens, Ramana Kumar
A verified type system for CakeML. IFL (2015)
Benja Fallenstein, Ramana Kumar
Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. ITP (2015)
Thomas Tuerk, Magnus O. Myreen, Ramana Kumar
Pattern Matches in HOL: - A New Representation and Improved Code Generation. ITP (2015)
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
CakeML: a verified implementation of ML. POPL (2014)
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
HOL with Definitions: Semantics, Soundness, and a Verified Implementation. ITP (2014)
Magnus O. Myreen, Scott Owens, Ramana Kumar
Steps towards Verified Implementations of HOL Light. ITP (2013)
Ramana Kumar
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. PxTP@CADE (2013)
Ramana Kumar, Joe Hurd
Standalone Tactics Using OpenTheory. ITP (2012)
Naghmeh Ghafari, Ramana Kumar, Jeff Joyce, Bernd Dehning, Christos Zamantzas
Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study. FMICS (2011)
Ramana Kumar, Tjark Weber
Validating QBF Validity in HOL4. ITP (2011)
Ramana Kumar, Michael Norrish
(Nominal) Unification by Recursive Descent with Triangular Substitutions. ITP (2010)