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 is interesting, because it permits arbitrary recursion in definitions, allowing even non-terminating or circular definitions as terms in the logic, which means it can express arbitrary computation despite being only a first-order arithmetic. To remain consistent, Grounded Arithmetic weakens many inference rules compared to classical arithmetic. Besides the axiomatization of the logic and arithmetic theory itself, I formalized a fair bit of basic arithmetic from the axioms, including Cantor tuples and associated machinery, in order to be able to embed inductive datatypes into the natural number theory. A case study then provided a fully verified encoded List datatype, with all required theorems proven in Grounded Arithmetic itself. Advised by Bryan Ford:

Formalizing Grounded Arithmetic atop Isabelle/Pure