Who I am

Face Shot

I am a second year graduate student in computer science at the University of Washington focusing on Programming Languages and Software Engineering. My main interest is in making programming and verification with dependent types more accessible through better proof engineering tools and practices.

In general, I enjoy using elegant theory to design and build tools with concrete applications. My current project makes use of categorical models of dependent type theory, but also involves building a compiler and reasoning about real code.


Current Research

I am currently working with Dan Grossman and Nate Yazdani on making proof assistants like Coq easier to use. Programming in these proof assistants is fragile -- small changes in theorems can break proofs that depend on those theorems. We are using information from changes in the proofs of those theorems to generate patches for broken proofs that depend on those theorems. This is essentially program repair for dependently typed languages.

I recently finished an internship with the Automated Reasoning Group at Amazon with Serdar Tasiran and Daniel Schwartz-Narbonne. I developed a solver-aided domain-specific language to help developers write better tests for web services. As part of this work, I extended Rosette to handle strings and regular expressions.



I am a competitive runner and triathlete. I run for Club Northwest. I occasionally write articles for Northwest Runner.

I am the writer and interviewer behind The Identity Function, a blog interview series about LGBTQ computer science researchers.

I enjoy singing and composing music for the piano.