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 making it easier to maintain verified programs through better proof engineering technologies. To that end, I develop foundational results in dependent type theory, and use those results to drive the development of tools informed by the needs of real proof engineers. 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 June 2021. Here are my materials. 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.