Dr. Ramana Kumar

Ramana Kumar, Ph.D. is a researcher at Data61, CSIRO / UNSW.
 
His papers include Proof-producing reflection for HOL, with an application to model polymorphism, Proof-grounded bootstrapping of a verified compiler: producing a verified read-eval-print loop for CakeML, Self-formalisation of higher-order logic, HOL with definitions: semantics, soundness, and a verified implementation, CakeML: a verified implementation of ML, Challenges in using OpenTheory to transport Harrison’s model from HOL Light to HOL4, Steps towards verified implementations of HOL Light, Standalone tactics using OpenTheory, Validating QBF validity in HOL4, Formal verification of real-time data processing of the LHC beam loss monitoring system: a case study, (Nominal) Unification by recursive descent with triangular substitutions, and A shallow Scheme embedding of bottom-avoiding streams.
 
Ramana earned his PhB in Computer Science (First Class Honors) at The Australian National University in 2010. He earned his MPhil ACS at the University of Cambridge in 2011. He earned his Ph.D. at the University of Cambridge in 2016 with the dissertation Self-compilation and Self-verification.