Projects

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.

  • Together with Simon Peyton Jones and Richard Eisenberg we extended GHC with injective type families. Details are described in the paper Injective Type Families for Haskell.

  • 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.

• singletons (github, hackage)
  Together with Richard Eisenberg I developed a method of converting Haskell term-level functions to the type level. Our approach is implemented in the singletons library.

• Dreamcast GDMenu maker script for Linux (github)
  A simple bash script for preparing an SD memory card to be used with GDEMU optical drive emulator for the Sega Dreamcast console. Born out of frustration that the only existing tools were for Windows.

• Phantasy Star Online section ID calculator (github)
  A simple utility for computing section ID assigned to player character in Phantasy Star Online. Once again a product of frustration that there are only Windows and online tools, but no native Linux cli tools.

• Free IPS Patcher (bitbucket)
  A simple Linux cli tool for applying IPS patches. Written because I was tired of using online patchers.

• 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.

• haskell-testing-stub (bitbucket)
  A small stub project that demonstrates how to organize tests and benchmarks in a Haskell project.

• tasty-program (bitbucket, hackage)
  Library that extends tasty testing framework. Allows to test whether a given program executes successfully.

• tasty-hunit-adapter (bitbucket, hackage)
  Library that extends tasty testing framework. Allows to import existing HUnit tests.