(Nominal) Unification by Recursive Descent with Triangular Substitutions. - Ramana Kumar; Michael Norrish (ITP, 2010)

Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study. - Naghmeh Ghafari; Ramana Kumar; Jeff Joyce; Bernd Dehning; Christos Zamantzas (FMICS, 2011)

Validating QBF Validity in HOL4. - Ramana Kumar; Tjark Weber (ITP, 2011)

Standalone Tactics Using OpenTheory. - Ramana Kumar; Joe Hurd (ITP, 2012)

Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. - Ramana Kumar (PxTP@CADE, 2013)

Steps towards Verified Implementations of HOL Light. - Magnus O. Myreen; Scott Owens; Ramana Kumar (ITP, 2013)

HOL with Definitions: Semantics, Soundness, and a Verified Implementation. - Ramana Kumar; Rob Arthan; Magnus O. Myreen; Scott Owens (ITP, 2014)

CakeML: a verified implementation of ML. - Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens (POPL, 2014)

A verified type system for CakeML. - Yong Kiam Tan; Scott Owens; Ramana Kumar (IFL, 2015)

Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. - Benja Fallenstein; Ramana Kumar (ITP, 2015)

Pattern Matches in HOL: - A New Representation and Improved Code Generation. - Thomas Tuerk; Magnus O. Myreen; Ramana Kumar (ITP, 2015)

Functional Big-Step Semantics. - Scott Owens; Magnus O. Myreen; Ramana Kumar; Yong Kiam Tan (ESOP, 2016)

A new verified compiler backend for CakeML. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (ICFP, 2016)

A Proof Strategy Language and Proof Script Generation for Isabelle. - Yutaka Nagashima; Ramana Kumar (CoRR, 2016)

Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. - Ramana Kumar; Rob Arthan; Magnus O. Myreen; Scott Owens (J. Autom. Reason., 2016)

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. - Yutaka Nagashima; Ramana Kumar (CADE, 2017)

Verified compilation of CakeML to multiple machine-code targets. - Anthony C. J. Fox; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar (CPP, 2017)

Verified Characteristic Formulae for CakeML. - Armaël Guéneau; Magnus O. Myreen; Ramana Kumar; Michael Norrish (ESOP, 2017)

Verifying efficient function calls in CakeML. - Scott Owens; Michael Norrish; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2017)

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. - Son Ho; Oskar Abrahamsson; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan; Michael Norrish (IJCAR, 2018)

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). - Ramana Kumar; Eric Mullen; Zachary Tatlock; Magnus O. Myreen (ITP, 2018)

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. - Hugo Férée; Johannes Åman Pohjola; Ramana Kumar; Scott Owens; Magnus O. Myreen; Son Ho (VSTTE, 2018)

Verified Certificate Checking for Counting Votes. - Milad K. Ghale; Dirk Pattinson; Ramana Kumar; Michael Norrish (VSTTE, 2018)

Clocked Definitions in HOL. - Ramana Kumar; Magnus O. Myreen (CoRR, 2018)

Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (CoRR, 2018)

Modeling AGI Safety Frameworks with Causal Influence Diagrams. - Tom Everitt; Ramana Kumar; Victoria Krakovna; Shane Legg (AISafety@IJCAI, 2019)

Verified compilation on a verified processor. - Andreas Lööw; Ramana Kumar; Yong Kiam Tan; Magnus O. Myreen; Michael Norrish; Oskar Abrahamsson; Anthony C. J. Fox (PLDI, 2019)

The verified CakeML compiler backend. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (J. Funct. Program., 2019)

REALab: An Embedded Perspective on Tampering. - Ramana Kumar; Jonathan Uesato; Richard Ngo; Tom Everitt; Victoria Krakovna; Shane Legg (CoRR, 2020)

Avoiding Tampering Incentives in Deep RL via Decoupled Approval. - Jonathan Uesato; Ramana Kumar; Victoria Krakovna; Tom Everitt; Richard Ngo; Shane Legg (CoRR, 2020)

Proof-Producing Synthesis of CakeML from Monadic HOL Functions. - Oskar Abrahamsson; Son Ho; Hrutvik Kanabar; Ramana Kumar; Magnus O. Myreen; Michael Norrish; Yong Kiam Tan (J. Autom. Reason., 2020)

Formal Methods for the Informal Engineer: Workshop Recommendations. - Gopal Sarma; James Koppel; Gregory Malecha; Patrick Schultz; Eric Drexler; Ramana Kumar; Cody Roux; Philip Zucker (CoRR, 2021)

TacticToe: Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (J. Autom. Reason., 2021)

Reward tampering problems and solutions in reinforcement learning: a causal influence diagram perspective. - Tom Everitt; Marcus Hutter; Ramana Kumar; Victoria Krakovna (Synth., 2021)

Verified Compilation and Optimization of Floating-Point Programs in CakeML. - Heiko Becker; Robert Rabe; Eva Darulova; Magnus O. Myreen; Zachary Tatlock; Ramana Kumar; Yong Kiam Tan; Anthony C. J. Fox (ECOOP, 2022)

Candle: A Verified Implementation of HOL Light. - Oskar Abrahamsson; Magnus O. Myreen; Ramana Kumar; Thomas Sewell (ITP, 2022)

Safe Deep RL in 3D Environments using Human Feedback. - Matthew Rahtz; Vikrant Varma; Ramana Kumar; Zachary Kenton; Shane Legg; Jan Leike (CoRR, 2022)

Goal Misgeneralization: Why Correct Specifications Aren't Enough For Correct Goals. - Rohin Shah; Vikrant Varma; Ramana Kumar; Mary Phuong; Victoria Krakovna; Jonathan Uesato; Zac Kenton (CoRR, 2022)

Solving math word problems with process- and outcome-based feedback. - Jonathan Uesato; Nate Kushman; Ramana Kumar; H. Francis Song; Noah Y. Siegel; Lisa Wang; Antonia Creswell; Geoffrey Irving; Irina Higgins (CoRR, 2022)

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). - Heiko Becker; Robert Rabe; Eva Darulova; Magnus O. Myreen; Zachary Tatlock; Ramana Kumar; Yong Kiam Tan; Anthony C. J. Fox (Dagstuhl Artifacts Ser., 2022)

Scaling Goal-based Exploration via Pruning Proto-goals. - Akhil Bagaria; Ray Jiang; Ramana Kumar; Tom Schaul (CoRR, 2023)

Explaining grokking through circuit efficiency. - Vikrant Varma; Rohin Shah; Zachary Kenton; János Kramár; Ramana Kumar (CoRR, 2023)

Cakes That Bake Cakes: Dynamic Computation in CakeML. - Thomas Sewell; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar; Alexander Mihajlovic; Oskar Abrahamsson; Scott Owens (Proc. ACM Program. Lang., 2023)

Discovering agents. - Zachary Kenton; Ramana Kumar; Sebastian Farquhar; Jonathan Richens; Matt MacDermott; Tom Everitt (Artif. Intell., 2023)

Discovering Agents (Abstract Reprint). - Zachary Kenton; Ramana Kumar; Sebastian Farquhar; Jonathan Richens; Matt MacDermott; Tom Everitt (AAAI, 2024)

Evaluating Frontier Models for Dangerous Capabilities. - Mary Phuong; Matthew Aitchison; Elliot Catt; Sarah Cogan; Alexandre Kaskasoli; Victoria Krakovna; David Lindner; Matthew Rahtz; Yannis Assael; Sarah Hodkinson; Heidi Howard; Tom Lieberum; et al. (CoRR, 2024)