Ramana Kumar

Available identifiers

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	2024-01-26	Paper
Discovering agents	2023-08-28	Paper
TacticToe: learning to prove with tactics	2021-06-09	Paper
Proof-producing synthesis of CakeML from monadic HOL functions	2020-11-02	Paper
The verified CakeML compiler backend	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	2017-05-19	Paper
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation	2016-05-26	Paper
Proof-Producing Reflection for HOL	2015-09-14	Paper
Pattern Matches in HOL:	2015-09-14	Paper
HOL with Definitions: Semantics, Soundness, and a Verified Implementation	2014-09-08	Paper
CakeML	2014-04-10	Paper
Steps towards Verified Implementations of HOL Light	2013-08-07	Paper
Standalone Tactics Using OpenTheory	2012-09-20	Paper
Validating QBF Validity in HOL4	2011-08-17	Paper
(Nominal) Unification by Recursive Descent with Triangular Substitutions	2010-09-14	Paper

This page was built for person: Ramana Kumar