Ramana Kumar

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