Skip to main content

Ramana Kumar

Ramana Kumar
Researcher

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
Email:Ramana.Kumar@data61.csiro.au

More contact information is available at the Contact page.

Photo of Ramana Kumar

Publication List

Projects

Current

Past

Publications

Data61 Papers

2016

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

NICTA Papers

2016

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

Non-NICTA Papers

2016

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