| 2024 | AAAI | Discovering Agents (Abstract Reprint). | Zachary Kenton, Ramana Kumar, Sebastian Farquhar, Jonathan Richens, Matt MacDermott, Tom Everitt |
| 2022 | ECOOP | 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 |
| 2022 | ITP | Candle: A Verified Implementation of HOL Light. | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
| 2019 | IJCAI | Modeling AGI Safety Frameworks with Causal Influence Diagrams. | Tom Everitt, Ramana Kumar, Victoria Krakovna, Shane Legg |
| 2019 | PLDI | Verified compilation on a verified processor. | Andreas Lw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox |
| 2018 | CADE | 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 |
| 2018 | ITP | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). | Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen |
| 2017 | CADE | A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. | Yutaka Nagashima, Ramana Kumar |
| 2017 | CPP | Verified compilation of CakeML to multiple machine-code targets. | Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
| 2017 | ESOP | Verified Characteristic Formulae for CakeML. | Armal Guneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish |
| 2016 | ESOP | Functional Big-Step Semantics. | Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan |
| 2016 | ICFP | A new verified compiler backend for CakeML. | Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish |
| 2015 | ITP | Proof-Producing Reflection for HOL - With an Application to Model Polymorphism. | Benja Fallenstein, Ramana Kumar |
| 2015 | ITP | Pattern Matches in HOL: - A New Representation and Improved Code Generation. | Thomas Tuerk, Magnus O. Myreen, Ramana Kumar |
| 2014 | ITP | HOL with Definitions: Semantics, Soundness, and a Verified Implementation. | Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens |
| 2014 | POPL | CakeML: a verified implementation of ML. | Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens |
| 2013 | CADE | Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. | Ramana Kumar |
| 2013 | ITP | Steps towards Verified Implementations of HOL Light. | Magnus O. Myreen, Scott Owens, Ramana Kumar |
| 2012 | ITP | Standalone Tactics Using OpenTheory. | Ramana Kumar, Joe Hurd |
| 2011 | FMICS | 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 |
| 2011 | ITP | Validating QBF Validity in HOL4. | Ramana Kumar, Tjark Weber |
| 2010 | ITP | (Nominal) Unification by Recursive Descent with Triangular Substitutions. | Ramana Kumar, Michael Norrish |