Below is a list of projects and libraries I have been involved with.
Skye: A programming language bridging theory and practice for scientific data curation (project homepage)
I worked together with Frank Emrich, Sam Lindley, James Cheney and Jonathan Coates on design of FreezeML, an extension of ML with first-class polymorphism. This system was then implemented in the Links programming language. Details are described in FreezeML: Complete and Easy Type Inference for First-Class Polymorphism paper.
I developed a prototype implementation of provenance tracking as a software library, which is unlike earlier implementations that were compiler extensions. Details are described in Language-integrated provenance in Haskell paper. Implementation is available on github.
I worked together with Wilmer Ricciotti, Roly Perera and James Cheney on slicing imperative functional programs. Details are described in Imperative Functional Programs That Explain Their Work paper. Implementation is available on github.
I designed a slicing algorithm for Imp, an imperative toy programming language, and formally proved correctness of my algorithm in Coq. Details are described in Verified Self-Explaining Computation paper. Implementation is available on bitbucket.
I contributed numerous patches to Links programming language.
Glasgow Haskell Compiler (project homepage)
I have been involved in development of GHC between 2013 and 2016.
I contributed various patches to Template Haskell.
I implemented new PrimOps for comparing built-in primitive types. These PrimOps allow writing branchless comparisons required in certain high-performace computations. See GHC wiki for an in-depth discussion of the problem and implementation details.
I worked on improving GHC’s Cmm optimization pipeline.
dep-typed-wbl-heaps (tutorial (pdf), bitbucket: Agda code, Haskell code)
Verified implementation of a weight biased leftist heap in Agda and Haskell. This project is a an intermediate-level tutorial aimed at people who already have a basic knowledge on program verification using dependent types.
A small stub project that demonstrates how to organize tests and benchmarks in a Haskell project.