The following is a list of software that I have been involved in developing as part of my academic research activties.

Rotor

Rotor is a protoype automatic refactoring tool for the OCaml programming language. Currently, it supports renaming of top-level values within modules. Joe Harrison and Steven Varoumas are currently working on implementing other kinds of refactoring. We have had support from Jane Street in London.

Rotor is currently hosted on Gitlab and is published in the OPAM package repository for OCaml.

Please visit Rotor’s homepage for more details.

Cyclist

Cyclist is a framework for building automatic deductive verifiers based on cyclic proofs. It contains a suite of related tools making use of the symbolic heap fragment of Separation Logic. These include: an entailment prover and disprover; a satisfiability checker; a model checker; a (termination) verifier for simple imperative programs with loops and recursive procedures; a verifier for temporal properties of simple imperative programs with loops; and a tool for abducing inductive predicates and sufficient conditions for memory-safe (terminating) execution of simple imperative programs with loops; It also includes an entailment prover for inductive definitions over first-order logic with successor.

Cyclist was originally developed by Nikos Gorogiannis and is hosted on Github. Please visit Cyclist’s homepage for more details.

DecML OCaml Extension

DecML is a PPX extension for the OCaml programming language that implements the abductive calculus described in this paper. Further details can be found in this technical report. It allows machine learning models to be specified as functions with specially marked constants denoting tunable parameters. These constants can then be ‘decoupled’ from the function, to give a parameterised function that can be used to learn the correct value of the parameters using observed data (e.g. using gradient descent).

The extension is hosted on Github.

An alternative implementation was developed by Victor Darvariu for his MSci dissertation.

RAG Parser

The recursive adaptive grammar (RAG) formalism was devised by John Shutt. It is a grammar formalism for declaratively specifying arbitrary, recursively enumerable languages. A recursive adaptive grammar can be seen as a kind of attribute grammar, in which each non-terminal is synthesises a single (semantic) attribute. The expressive power derives from a query operator, which allows a synthesised attribute to be treated and parsed as syntax.

I constructed and implemented a RAG parsing algorithm. It is hosted on Github.