Open Source

Checker Framework / type systems, static analysis

Active contributor to the Checker Framework and Checker Framework Inference, including a JSpecify nullness checking mode and an immutability checker, plus soundness bug fixes and pull-request review.

PICO / Rocq proof

Mechanized proof artifact for the PICO Java immutability type system: Rocq proof.