Who I am

Face Shot

I am a third 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.



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 interactive theorem provers like Coq easier to use. Programming in these provers is brittle: Small changes can break many dependent proofs. Our vision is a future of proof automation in interactive theorem provers that automatically adapts proofs to breaking changes. Our prototype tool PUMPKIN PATCH generalizes an example adaptation into a reusable patch that can fix broken proofs.



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.