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. I am also a research scientist intern with Byron Cook's formal methods research group at Amazon.

I'm interested in the connections and interactions between different modes of reasoning (Curry-Howard is a special case of this). Any work that unifies seemingly disparate ideas in PL will have me very excited. Appropriately, I'm drawn to both the type theoretic, constructive school of verification and the classical, SMT-based school of verification and synthesis. I have a secondary interest in security.


Current Research

I am currently working with the Automated Reasoning Group at Amazon with Serdar Tasiran and Daniel Schwartz-Narbonne. I am generating tests for developers from a specification of service inputs using a solver-aided intermediate language. The language can express to the solver what it means for values to be different and to cover a specification a certain way. As part of this work, I am extending Rosette to handle strings and regular expressions.

In the future, I plan to look into a more general way of combining theories than Nelson-Oppen which allows SMT solvers to take advantage of mathematical properties like inverse functions between two theories.

I have also been thinking extensively about how to implement a higher-order logic solver for dependent type theory. I would love to chat with anyone who is interested in the connections between logic and DTT.



I am a competitive runner and triathlete. I run for Club Northwest. I am also on the board. 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.