A substantial part of my time is devoted to designing and writing software, in particular software that proves things about other formal artifacts: programs, formulas of logic, mathematical theorems, etc. This comprises work on a bestiary of systems that includes proof checkers, interactive theorem provers, and increasingly compilers and interpreters. Some of this work is publicly available as free and open source software, while more experimental and embryonic branches patiently bid their time.

  • Recently, I am giving plentiful thought to the proof assistant Abella: both in relatively self-contained but useful features and technical improvements; and in large, ongoing modifications to the kernel of the system.

  • Many smaller projects are directly related to the declared goal of ProofCert of universal production, communication (i.e., reuse) and checking (i.e., trust) of proof evidence. Families of proof checkers (minimalistic or not, correct by construction or certified), as well as foundational proof certificate formats, belong here.

  • Last year, I commenced work on a gradually typed flavor of the Ruby programming language, similar in spirit to recent developments for other dynamic languages like TypeScript — though incubating my dissertation presently keeps me from revisiting it. The original proposal was supported by Google Summer of Code 2016.