Software & Projects

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
Typelevel homepage

Typelevel

Contributor to & maintainer of various Typelevel projects, including:

Screenshot of typelevel.org, Copyright © 2013–2017 its contributors
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 paper 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.