Back in 2014, I designed (with Leo White) and began to implement a multicore runtime for the OCaml programming language, which I worked on sporadically as a means of avoiding my PhD work. I've now finished my PhD, and KC Sivaramakrishnan (who worked on the impressive MultiMLton project) has joined the effort, so this project is finally getting the attention it deserves. (The first 90% of the work is done, so we only have the remaining 90% and then the final 90% left to do).

Recently, I've been working on a memory model for parallel OCaml programs, which specifies the behaviour of programs sharing mutable locations between threads, balancing performance and the ability to reason about code.

Multicore OCaml development happens on github.

My PhD (supervised by the wonderful Alan Mycroft) was on cleanly integrating type inference with subtyping, allowing functional and object-oriented programming techniques to be seamlessly combined.

The result is a type inference algorithm in the Hindley-Milner vein, which manages to infer compact principal types even in the presence of record subtyping and co-/contra-variance. Technically, this involved taking an algebraic approach to the definition of subtyping and introducing biunification, an analogue of unification that works with subtyping constraints.

You can read my thesis, read the POPL paper, see a prototype type checker, or get the code.

Malfunction is an untyped program representation, suitable as a compilation target for functional languages. It's a thin wrapper around the Lambda intermediate language of OCaml, providing a means for other languages to target the mature OCaml back-end.

I presented it at the ML Workshop 2016, along with a prototype backend for the Idris programming language, which significantly outperformed Idris' native C backend. Currently, Frederik Hanghøj Iversen and Jan Mas Rovira are working on a Malfunction back-end for Agda

jq is a command-line tool for filtering, transforming, and generally mangling JSON data. It's designed to be concise and easy to use for simple tasks, but if you dig a little deeper you'll find a featureful functional programming language hiding underneath. It's become widely used. As well as the jq manual, there are many tutorials floating around the internet, of which my favourite is this talk by Bob Tiernay.

These days, jq is maintained by Nicolas Williams, William Langford and a large ensemble cast.

Paper published at POPL 2017, with Alan Mycroft. Covers type inference with principal types for a simple core ML calculus with subtyping, including some of the results from my thesis. [pdf] [slides] [extended slides]

My thesis. Presents a type system (the first!) combining ML-style parametric polymorphism and subtyping, with type inference, principal types and decidable type subsumption. [abstract] [pdf]

Talk given at SPLS Nov '16. By careful abuse of Agda's proof-irrelevance, we can use some classical principles like Markov's principle while remaining constructive. During the talk, we ran into a soundness bug in Agda! (which was quickly fixed when reported).

Talk given at the ML Workshop 2016. Introduces Malfunction, explains why the OCaml back-end is a good candidate for reuse, and gives some preliminary results from a new Idris back-end. [pdf] [talk]

Report from the Dagstuhl seminar on algebraic effects. Matija Pretnar, Leo White, KC Sivaramakrishnan and I worked out some details of how to introduce effect typing to OCaml, and collaborated on a toy implementation. Later, Leo integrated effect typing with the real OCaml typechecker, and gave a talk at HOPE 2016. [pdf] [code]

Talk given at S-REPLS 3, about what was then work-in-progress on subtyping and type inference.

Talk given at the ML Workshop 2015, which later became a POPL paper. With Alan Mycroft. [pdf] [talk]

Talk given at the OCaml Workshop 2014, about the design of the multicore OCaml runtime. With Leo White and Anil Madhavapeddy. [pdf] [talk]

Paper published at ICFP 2013. I show how a single small piece of code implementing the 'closure' operation on a semiring can find shortest paths, analyse data flow, pack knapsacks and simulate Petri nets. Selected as a SIGPLAN Research Highlight. [pdf] [slides]

A rant delivered at the Cambridge LLVM Day, about the inadequacy of LLVM's gcroot interface for high-performance garbage collectors. (A bit dated now: the new 'statepoints' interface looks much better designed, although it's still experimental). [slides]

Unpublished. Shows how to simulate a Turing machine using just the x86 mov instruction (and one unconditional branch). Chris Domas took the joke a bit too far by actually implementing it in a C compiler, and gave a talk about it. [pdf]

Paper published in ACM TACO and presented at HiPEAC 2013, with Servesh Muralidharan and David Gregg. We found that by adding context-switching as a language primitive rather than a library feature, we can do extremely efficient user-level concurrency. [paper]