PICO / Java immutability
Developing an optional type checker for Java immutability, with Rocq formalization work for soundness and related safety properties.
Research
I care about static guarantees that survive contact with real codebases: precise enough to prove useful properties, and practical enough to fit into the way developers already write, review, and debug programs.
Checker Framework / static analysis
Contributing features and maintenance work to the Checker Framework and Checker Framework Inference, including improvements around Nullness and Initialization checking.