Ramana Kumar

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Candle: a verified implementation of HOL light	2024-07-15	Paper
Reward tampering problems and solutions in reinforcement learning: a causal influence diagram perspective Synthese	2024-01-26	Paper
Discovering agents Artificial Intelligence	2023-08-28	Paper
TacticToe: learning to prove with tactics Journal of Automated Reasoning	2021-06-09	Paper
Proof-producing synthesis of CakeML from monadic HOL functions Journal of Automated Reasoning	2020-11-02	Paper
The verified CakeML compiler backend Journal of Functional Programming	2019-11-22	Paper
Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions	2018-10-18	Paper
Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)	2018-10-04	Paper
A proof strategy language and proof script generation for Isabelle/HOL	2017-09-22	Paper
Verified characteristic formulae for CakeML Programming Languages and Systems	2017-05-19	Paper
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation Journal of Automated Reasoning	2016-05-26	Paper
Proof-producing reflection for HOL. With an application to model polymorphism Interactive Theorem Proving	2015-09-14	Paper
Pattern matches in HOL: a new representation and improved code generation Interactive Theorem Proving	2015-09-14	Paper
HOL with definitions: semantics, soundness, and a verified implementation Interactive Theorem Proving	2014-09-08	Paper
CakeML Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages	2014-04-10	Paper
Steps towards Verified Implementations of HOL Light Interactive Theorem Proving	2013-08-07	Paper
Standalone Tactics Using OpenTheory Interactive Theorem Proving	2012-09-20	Paper
Validating QBF Validity in HOL4 Interactive Theorem Proving	2011-08-17	Paper
(Nominal) unification by recursive descent with triangular substitutions Interactive Theorem Proving	2010-09-14	Paper

Research outcomes over time

This page was built for person: Ramana Kumar