Rohan Jacob-Rao
I just finished writing my Masters thesis! Thanks to my advisor Prof. Brigitte Pientka. I will graduate from McGill University with an M.Sc. in Computer Science.
My specialties are programming language design and software verification. In essence, I study tools for writing correct programs.
My thesis describes an indexed type system with recursion at both the term and type levels. Perhaps surprisingly, I prove that all programs in this language terminate (i.e. infinite loops are impossible to write). This project provides partial justification for the use of Beluga as a proof assistant.
I've written a couple of papers on this topic with co-authors Brigitte Pientka and Andrew Cave.
Mechanizing Proofs about Mendler-style Recursion
pdf code
accepted at LFMTP 2016 in Porto, Portugal.
Index-Stratified Types draft
During my Masters, I completed two internships at Facebook. My first project was on Infer, an open-source static analysis tool written in the awesome OCaml language. My second project was to improve performance of Facebook's distributed video encoding.
Before McGill, I was a research engineer at NICTA, now called Data61. I worked on formal verification of C programs using the AutoCorres tool. I am also an alumnus of UNSW Mathematics and Computer Science. My full CV is here.