Mr Hrutvik Kanabar
I do not currently have any publications!
However, my undergraduate dissertation can be found here. For this third-year project, I implemented and verified a compiler optimisation for the CakeML compiler. I was supervised by Magnus Myreen (who supervised the technical aspects of the project and CakeML), Anthony Fox (who taught me the basics of HOL), and Stephen Kell (who supervised project planning and dissertation writing). This is what led me to my current PhD work!
PhD Project Summary
My PhD is on "Building Verified Applications in CakeML", supervised by Scott Owens.
CakeML is an open-source, functional programming language, verified compiler, and proof ecosystem. The CakeML language is ML-like, and the semantics and compiler algorithm are specified using the interactive theorem-prover HOL. The compiler has been proven to preserve code semantics end-to-end (from source code to machine code), and can bootstrap itself.
My work is focused on techniques for formally verifying applications written in CakeML - enabling specification and verification of their behaviour. My current aim is to work on the problem of program equivalence in CakeML. The (eventual) use case is as follows:
- Replace existing safe CakeML library code (e.g. array sorting) with potentially unsafe code (e.g. turn off array bounds checking).
- Prove program equivalence of the safe and unsafe code, using my work.
- Result: unsafe, optimised code in a safe, end-to-end verified compiler!
I am currently reading into logical relations and separation logic (see below) - I hope to apply these to program equivalence in CakeML.
I am a member of the following research groups:
I am currently involved in an effort to improve the "monadic translator" in CakeML, with Oskar Abrahamsson and other CakeML developers. This machinery allows translation of pure functions written in the higher-order logic of HOL into stateful CakeML, using a state-and-exception monad. Each translation is proof-producing: a theorem is generated which states that the generated CakeML code has the same behaviour as the HOL function. This is a key part of bootstrapping the compiler, and allows for more efficient (but still verified) compiler code.
I am also beginning to explore "logical relations": families of relations between terms of a programming language, indexed by types. These could be used to develop a notion of program equivalence within CakeML. I am involved in a reading group aiming to explore these, and we will be looking at the IRIS project soon.
Another area of interest is "characteristic formulae", which are separation logic formulae encapsulating the behaviour of a program. There is a characteristic formulae framework for CakeML, but this could be used/developed further to aid my exploration of program equivalence in CakeML.
Lastly, I am involved in a category theory reading group for interest!
I have previously led seminars in:
I am currently leading seminars in:
I studied at University of Cambridge before coming to Kent (2015 - 2018). In my first year I read Natural Sciences, before switching to Computer Science for my second and third years. My Director of Studies during these last two years was Tim Griffin. I will receive my B.A. (Hons) in June 2019.
I am currently coaching for University of Kent Rowing Club!