School of Computing

Mr Hrutvik Kanabar

Research Student

Photo of H Kanabar
  • Room SW103
    School of Computing
    University of Kent, CT2 7NF

Publications

I do not currently have any publications! A collaborative paper is currently under review at the Journal of Automated Reasoning (see below).

Recently, I placed second at the POPL 2020 Student Research Competition. This involved three rounds: an extended abstract, a poster, and a presentation.

You can also find my undergraduate dissertation here. In this third-year project I implemented and verified a compiler optimisation for the CakeML compiler. My supervisors were: Magnus Myreen (technical - CakeML), Stephen Kell (project planning and dissertation), and Anthony Fox (technical - HOL4). 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, ML-like programming language, verified compiler, and proof ecosystem. The CakeML language, semantics, and compiler algorithm are all specified in higher-order logic, using the interactive theorem-prover HOL4. This allows end-to-end verification of semantic-preservation for the compiler, and boostrapping in the logic.

My work

My project aims to create practical techniques for writing useful, verified CakeML applications. My current aim is to build a semantic type system for CakeML: this would reason about programs that behave as if they have a certain type, but are not syntactically typeable. Crucially, this semantic notion of typing must co-exist with the more common syntactic one. The canonical use case is:

  1. Write a fast CakeML library using unsafe (syntactically untypeable) code (e.g. array sorting using array accesses which are not bounds-checked).
  2. Prove that this library is semantically well-typed - i.e. it can safely be used at the intended type.
  3. Users should be able to write syntactically typeable code which calls this unsafe library with no added cost.
  4. Result: unsafe, optimised code in a safe, end-to-end verified compiler!

I am exploring a unary, step-indexed logical relation to solve this problem, taking inspiration from projects such as RustBelt. We believe this approach is general enough to allow for other interesting use cases (see below).

Research Interests

I am a member of the following research groups:

Current work - a logical relation for semantic typing in CakeML

The top-level CakeML compiler correctness theorem requires that any source program has a non-failing semantics (to permit greater optimisation). We enforce this condition in one of three ways:

Each of these present restrictions:
  • Syntactic typing prevents e.g. fast imperative programs which remove array bounds checks.
  • Translation from HOL requires functions to be specifiable in HOL - non-terminating programs are not expressible.
  • Separation logic proof requires a great deal of effort, even for programs which use a minimal amount of unsafety.

We would like a more general way of ensuring safety, which will ideally allow us to mix these three methods.

We plan to create a logical relation which will express a semantic type system for CakeML. By proving compatibility lemmas (semantic versions of each syntactic typing rule), we can compose syntactically typeable code and semantically typeable code with no added effort. We also aim to integrate this with the existing CakeML refinement invariants and characteristic formulae framework to some extent, so that we can re-use proofs in these frameworks for semantic typing proofs.

Our intended use cases are:

  • Permitting composition of safe and unsafe code.

    Provided unsafe code is well-encapsulated and so can be given a semantic type, this will allow for more performant code (see example above). This is a well-known use of semantic type systems.

  • Reasoning about type abstraction.

    Many modules hide their implementations using type abstraction, and so maintain internal invariants. Semantic typing is well-known as a way of reasoning about the preservation of these invariants.

    We aim to use this to prove soundness for Candle, a HOL theorem-proving kernel implemented in CakeML. Like all LCF-style kernels, Candle implements a core module which implements and hides a theorem datatype, exposing only primitive inference rules operating on this datatype. The strong typing of CakeML ensures that only the module can construct theorems, so all theorems must be created using only these primitive rules. Proving soundness of Candle therefore relies on proving the type abstraction holds.

  • Compiling languages with stronger type systems to CakeML.

    We aim to compile languages with stronger type systems (dependent typing, type classes, and so on) to CakeML in a verified way. Ideally each compilation will produce a semantic type judgement, preserving our ability to reason about the safety of compiled code and also compose it with code written in CakeML.

    For example, the Coq theorem-prover can (unsafely) extract code to OCaml. The weaker type system of OCaml necessitates insertion of unsafe casts in the extracted code, losing formal proof of safety. However, a verified extraction to CakeML could preserve safety using our semantic type system. This would also allow composition with our compiler correctness theorem, and so enable a verified compilation pipeline from Coq to target code. For this, we would take inspiration from projects such as CertiCoq and Coq Coq Correct!.


Previous work - translation from higher-order logic to stateful CakeML

This work is under review for a special issue of the Journal of Automated Reasoning (JAR).

I was involved in an effort to improve CakeML's monadic translator, with Oskar Abrahamsson and other CakeML developers. This machinery translates higher-order logic functions written in a state-and-exception monad to stateful CakeML, allowing for generation of more efficient code. As with CakeML's pure translator, each translation produces a proof that the generated CakeML correctly implements the HOL function. These translators are key to bootstrapping the CakeML compiler.

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.


Other

I am involved in Lambda Club and a type theory reading group for interest!


Teaching

I have previously led seminars in:

I am currently leading seminars in:


Education

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.


Other Interests

I am currently coaching for University of Kent Rowing Club!

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 07/04/2020