Talia Ringer

I am a Ph.D candidate in computer science at the University of Washington focusing on Programming Languages and Software Engineering. My main interest is in making verification in interactive theorem provers easier through better proof engineering tools and practices, especially for proof maintenance. My goal is to develop a new generation of proof automation that helps proof engineers not only write, but also maintain proofs as the programs they verify change over time. My vision is a future where verification is accessible to all programmers with the help of these technologies.

I am currently applying for faculty positions. I expect to graduate in spring 2021. I am interested in positions both in the US and abroad. Please reach out to me if you think I would be a good addition to your research group!

Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. REPLICA: REPL Instrumentation for Coq Analysis. CPP 2020. Talk Video.

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software, Foundations and Trends® in Programming Languages: Vol. 5: No. 2-3, pp 102-281. 2019. Errata, Q & A.

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. ITP 2019. Talk Video.

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.

I am currently partnering with Galois to integrate the PUMPKIN PATCH proof repair suite into the workflow of proof engineers. As part of this, I am extending PUMPKIN PATCH with new functionality, including tactic generation and support for many different kinds of repairs.

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, studying Russian, singing, writing poetry, and composing music for the piano.