Software & Projects

Typelevel homepage


Contributor to & maintainer of various Typelevel projects, including:

Screenshot of, Copyright © 2013–2017 its contributors
Two collaborating octocats

Open source software

I contribute to a variety of open source projects. Find the full list of my pull requests on GitHub.

Collabocats from GitHub, Copyright © 2013–2019 GitHub
Isabelle/jEdit window


A list of my Isabelle-related projects can be found here.
Screenshot of Isabelle/jEdit: License of Isabelle, License of jEdit
CakeML logo


I am developing a verified compiler from Isabelle/HOL to CakeML syntax trees. A list of publications and prototype downloads can be found here.

Contributor to Lem, a “tool for lightweight executable mathematics.”

CakeML logo: License of CakeML
Logo of FFFUU

Fancy Formal Firewall Universal Understander

Contributor to Cornelius Diekmann's Haskell tool (and corresponding formalization) to simplify iptables firewall rulesets. The research papers can be found here.
Diagram by Cornelius Diekmann
Leon interface


I have developed an extension to Leon that allows it to use Isabelle as a solver in the background. The research paper can be found here. The major challenges were system integration (this has since been extracted as a separate project, libisabelle) and translating Scala expressions into idiomatic Isabelle/HOL definitions without compromising correctness.