Mr Hrutvik Kanabar
I do not currently have any publications! However, I have submitted a paper to the Journal of Automated Reasoning (JAR) as part of a collaboration (see below) - this is currently under review.
In addition, 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), Stephen Kell (who supervised project planning and dissertation writing), and Anthony Fox (who taught me the basics of HOL). 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. This project is funded by the UK Research Institute in Verified Trustworthy Software Systems (VeTSS).
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 writing and formally verifying CakeML applications - enabling specification and verification of their behaviour. My current aim is to work on a semantic notion of types in CakeML, allowing reasoning about programs that behave as if they have a certain type, but are not syntactically typeable. Crucially, this semantic notion of types must co-exist with the more traditional syntactic one. The canonical (eventual) use case is as follows:
- Write a CakeML library which makes use of unsafe, syntactically untypeable code for performance (e.g. array sorting using array accesses which are not bounds-checked).
- Show that this library can safely be used at the intended type - i.e. it has a semantic type.
- A user can then write syntactically typeable code which makes use of this unsafe library, with no added cost to them.
- Result: unsafe, optimised code in a safe, end-to-end verified compiler!
I am currently trying to use step-indexed logical relations to solve this problem, taking inspiration from projects such as RustBelt. We hope that our approach is general enough to allow for other interesting use cases (see below).
I am a member of the following research groups:
Current work - a logical relation for CakeML
I am currently working towards a unary, step-indexed logical relation for CakeML, aiming to give a semantic notion to CakeML types. Logical relations are families of relations on program terms, often indexed by types.
The CakeML compiler correctness theorem assumes that the input program has a non-failing semantics - this is standard in an optimising compiler as it allows for greater optimisation. Currently, this condition is enforced by a type safety theory and a sound/complete type inferencer: typeable programs do not fail, and a type is inferred if and only if a program is typeable. However, syntactic typing can be too strong a restriction - there are non-failing programs which are not typeable, and we would like to compile these with all the guarantees that CakeML provides. In particular, fast imperative code often operates outside of these restrictions.
We aim to create a logical relation which will reason about when programs can safely be considered to have a certain type. This notion of types must be compatible with each syntactic type rule, allowing composition of typeable and untypeable code without any added effort. We would also like to integrate this with the existing characteristic formulae framework for CakeML to some extent. These are separation logic formulae encapsulating the behaviour of a program - we would like to be able to transfer proofs from this separation logic framework to our logical relation framework in a general way.
Our intended use cases are:
- Adding unsafe features to CakeML.
Provided any unsafe features are proven to be safely encapsulated via the logical relation, this could allow for more performant code (see above).
- Reasoning about module boundaries and data encapsulation.
We hope to be able to reason about data hidden by module boundaries, and prove that data invariants are preserved.
An example use case is Candle, the CakeML version of a HOL kernel. In the LCF tradition, HOL (and therefore Candle) uses a core trusted kernel which defines a theorem type and implements primitive inference rules. This module hides the theorem type, relying on the strong typing of ML (CakeML) to ensure that only it can construct theorems, and so ensure that all theorems are correctly formed from the primitive inference rules. In order to prove that all theorems derived by Candle are sound with respect to its logical axioms, we must show that the theorem datatype is correctly hidden by the kernel module.
- Compiling languages with stronger type systems to CakeML.
We would like to be able to compile languages with dependent types, type classes, and so on into CakeML, while preserving our ability to reason about their safety.
For example, the Coq theorem-prover can (unsafely) extract code to OCaml. As OCaml has a weaker type system than the logic of Coq, the extractor must insert unsafe casts in the OCaml code. This is considered "safe" because the extracted code type-checks in Coq, and so should not fail in OCaml. However, we are interested by the possibility of extracting to CakeML, and using our logical relation to reason about safety at the CakeML level.
Previous work - translation from higher-order logic to stateful CakeML
This work was submitted to the Journal of Automated Reasoning (JAR), and is currently under review.
I was previously 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.
In particular, I contributed the following:
- Support for monadic translation of functions with parametric polymorphism.
- Permitting definition and translation of functions whose termination may depend on the monadic state.
- More powerful proof automation and a simpler user-interface.
I am involved in category theory and type theory reading groups for interest!
I have previously led seminars in:
- CO322: Foundations of Computing I. First year course - foundations in: algebra, statistics, proofs, and set theory.
- CO545: Functional and Concurrent Programming. First year course - Erlang and the actor model, Haskell.
I am currently leading seminars in:
- CO518: Algorithms, Correctness and Efficiency. Second year course - data structures, sorting, graphs, big-O.
- CO519: Theory of Computing. Second year course - logic and proof, regular languages, CFGs, computability.
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.
You can also find a short CV here.
I am currently coaching for University of Kent Rowing Club!