As a research intern at UW, I designed and implemented a type system to prove the absence of resource leaks on collections of resources in Java. This is implemented as a checker in the excellent Java Checker Framework. Advised by Michael Ernst:

Resource Leak Checker For Collections

As a thesis intern at EPFL, I formalized a first-order arithmetic termed Grounded Arithmetic (based on the Grounded Deduction logic) in the Isabelle/Pure proof assistant. Grounded Arithmetic permits arbitrary recursion in definitions, allowing even non-terminating or circular definitions as terms in the logic. It can thus express arbitrary computation. To remain consistent in the presence of non-terminating terms, Grounded Arithmetic weakens many inference rules compared to classical arithmetic (its consistency was proven independently for a deep embedding in Isabelle/HOL). I axiomatized the logic atop the minimal Pure calculus and formalized a fair bit of basic arithmetic, including Cantor tuples and associated machinery. I also encoded inductive datatypes into the axiomatized natural number theory, providing a fully verified encoding of a List datatype, with all required theorems proven in Grounded Arithmetic itself. Advised by Bryan Ford:

Formalizing Grounded Arithmetic atop Isabelle/Pure