Who I am

Face Shot

I am a fourth 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 and less brittle through better proof engineering tools and practices, especially search and reuse technologies. My vision is a future where dependent types are accessible to all programmers with the help of these technologies.



Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting Proof Automation to Adapt Proofs. CPP 2018. Talk Video.

Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, and Serdar Tasiran. A Solver-Aided Language for Test Input Generation. OOPSLA 2017. Talk Video.

Talia Ringer, Dan Grossman, and Franziska Roesner. AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems. CCS 2016. Talk Video.


Current Research

I am currently working with Dan Grossman, Nate Yazdani, and John Leo on making dependent types easier to use. Our prototype tool PUMPKIN PATCH addresses brittleness by automatically searching for patches to fix broken proofs in Coq when dependencies change. We are currently extending it to automatically search for certain equivalences between types, then use the equivalences it finds to port functions and proofs between those types.



I am a competitive runner. I run for Club Northwest.

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

I enjoy making bagels, learning foreign languages (currently Russian), and singing and composing music for the piano.