Skip to main content

Ramana Kumar

Ramana Kumar

Research Interests

Ramana is interested in building systems with end-to-end functional correctness theorems, and in techniques for interactive theorem proving. He is a developer of CakeML, a verified ML-like programming language (i.e., language spec, and compiler and runtime), and wants to verify the combined system consisting of CakeML running on the seL4 verified OS. Ramana's long-term interest is ensuring that, when computer systems become substantially more powerful, their impact is beneficial.

Contact Details

Mobile: +61 401 313 753

More contact information is available at the Contact page.

Photo of Ramana Kumar

Publication List





Data61 Papers


Abstract PDF Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish
Verified characteristic formulae for CakeML
European Symposium on Programming, pp. 584-610, Uppsala, Sweden, April, 2017
Abstract PDF Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar
Verified compilation of CakeML to multiple machine-code targets
Certified Programs and Proofs 2017, pp. 125-137, Paris, France, January, 2017


Abstract PDF Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish
A new verified compiler backend for CakeML
International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016
Abstract PDF Yong Kiam Tan, Scott Owens and Ramana Kumar
A verified type system for CakeML
Implementation and application of functional and programming languages, pp. 12, Koblenz, Germany, July, 2016
Winner: 2016 Peter Landin Prize for best paper

NICTA Papers


Abstract PDF Scott Owens, Magnus Myreen, Ramana Kumar and Yong Kiam Tan
Functional big-step semantics
European Symposium on Programming, pp. 27, Eindhoven, The Netherlands, April, 2016