Ramana Kumar

According to our database1, Ramana Kumar authored at least 32 papers between 2010 and 2021.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2021
TacticToe: Learning to Prove with Tactics.
J. Autom. Reason., 2021

2020
Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason., 2020

Avoiding Tampering Incentives in Deep RL via Decoupled Approval.
CoRR, 2020

REALab: An Embedded Perspective on Tampering.
CoRR, 2020

2019
The verified CakeML compiler backend.
J. Funct. Program., 2019

Verified compilation on a verified processor.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Modeling AGI Safety Frameworks with Causal Influence Diagrams.
Proceedings of the Workshop on Artificial Intelligence Safety 2019 co-located with the 28th International Joint Conference on Artificial Intelligence, 2019

2018
Learning to Prove with Tactics.
CoRR, 2018

Clocked Definitions in HOL.
CoRR, 2018

Verified Certificate Checking for Counting Votes.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
Verifying efficient function calls in CakeML.
Proc. ACM Program. Lang., 2017

Verified Characteristic Formulae for CakeML.
Proceedings of the Programming Languages and Systems, 2017

Verified compilation of CakeML to multiple machine-code targets.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation.
J. Autom. Reason., 2016

A Proof Strategy Language and Proof Script Generation for Isabelle.
CoRR, 2016

A new verified compiler backend for CakeML.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Functional Big-Step Semantics.
Proceedings of the Programming Languages and Systems, 2016

2015
Pattern Matches in HOL: - A New Representation and Improved Code Generation.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Proof-Producing Reflection for HOL - With an Application to Model Polymorphism.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A verified type system for CakeML.
Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, 2015

2014
CakeML: a verified implementation of ML.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

HOL with Definitions: Semantics, Soundness, and a Verified Implementation.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
Steps towards Verified Implementations of HOL Light.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012
Standalone Tactics Using OpenTheory.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011
Validating QBF Validity in HOL4.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study.
Proceedings of the Formal Methods for Industrial Critical Systems, 2011

2010
(Nominal) Unification by Recursive Descent with Triangular Substitutions.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010


  Loading...