Software & Projects

Typelevel homepage

Typelevel

Contributor to & maintainer of various Typelevel projects, including:

Screenshot of typelevel.org, Copyright © 2013–2017 its contributors
Isabelle/jEdit window

Isabelle

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

CakeML

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

Leon

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.