Talia Ringer

How can we build a world in which programmers of all skill levels across all domains can prove the absence of costly or dangerous bugs in software systems---that is, formally verify them? I am an Assistant Professor with the PL/FM/SE group at Illinois, and I like to build proof engineering technologies to make that world a reality. In so doing, I love to use the whole toolbox---everything from dependent type theory to program transformations to neural proof synthesis---all in service of real humans.

Asterisks next to names indicate shared first or last authorship.

Cosmo Viola, Max Fan, and Talia Ringer. Proof Repair across Quotient Type Equivalences. Under Submission. 2024.

Talia Ringer. Proofs and Conversations. To appear in the AMS Early Career Notices in 2024.

Audrey Seo*, Chris Lam*, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. ITP 2024.

Dylan Zhang, Curt Tigges, Zory Zhang, Stella Biderman, Maxim Raginsky, and Talia Ringer. Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion. TMLR 2024. (2023 short whitepaper version here.)

Dylan Zhang, Emily First, and Talia Ringer. Getting More out of Large Language Models for Proofs. AITP 2023.

Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-Proof Generation and Repair with Large Language Models. ESEC/FSE 2023. Distinguished Paper Award.

Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner*, and Talia Ringer*. Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. ITP 2023.

Alex Sanchez-Stern*, Emily First*, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. Passport: Improving Automated Formal Verification Using Identifiers. TOPLAS Volume 45, Issue 2: No. 12, pp 1-30. Presented at PLDI 2023. Tool repository.

Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, and Yuriy Brun. Proofster: Automated Formal Verification. ICSE 2023 (Demo Track). Demo video, tool website.

Hannah Leung, Talia Ringer, and Chris Fletcher. Towards Formally Verified Path ORAM in Coq. CoqPL 2023.

Emily Ruppel*, Sihang Liu*, Elba Garza, Sukyoung Ryu, Alexandra Silva, and Talia Ringer. Long-Term Mentoring for Computer Science Researchers. Communications of the ACM (CACM): Volume 66: No. 5, pp 33-35. May 2023.

Seth Poulsen, Matthew West, and Talia Ringer. Autogenerating Natural Language Proofs for Proof Education. The Coq Workshop 2022.

Talia Ringer. Proof Repair. Ph.D. Thesis, University of Washington, 2021. Defense video.

Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. Proof Repair across Type Equivalences. PLDI 2021. Talk video.

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 exploring a number of exciting topics right now, all with an underlying theme of proof engineering, and especially proof automation. In addition to my wonderful lab, I have excellent collaborators at UW, UMass Amherst, Google Research, Galois, Berkeley Eleuther AI, and other institutions with whom I'm super fortunate to explore these topics:

Proof Repair: How can we extend proof repair to make it more powerful and practical, so that it reaches proof engineers of all levels of expertise, across many different domains? I have several collaborations exploring this question, with techniques ranging from dependent type theory and proof term transformations to machine learning.

Machine Learning for Proofs: What can machine learning do for proof engineers, and how can this advance the state of the art in machine learning? What would it take to make machine learning tools for proofs much more practical---to infer and apply deep semantic relations, and to handle the tasks most difficult for proof engineers? How can we use machine learning to help people not just prove, but also specify what they want to prove to begin with? This is an exciting and hot topic I'm having a lot of fun exploring with many collaborators.

Proof Engineering: How can we advance the state of the art in proof engineering, and use it to drive the development of large, secure, and robust verified software and hardware systems? I have two collaborations exploring new domains and new kinds of proof engineering, looking at everything from compilation of proofs to verification of critical security properties of hardware.

I lead the Illinois Theorem Provers (ITP) lab (huge credit to Yao Li for the name), part of the PL/FM/SE group. Current members:

1. Kiran Gopinathan (postdoc),
2. Cosmo Viola (Ph.D.),
3. Chris Lam (Ph.D.),
4. Hannah Leung (Ph.D., coadvised with Christopher Fletcher),
5. Jilin Hu (visiting Ph.D.),
6. Evan Marzion (researcher),
7. Eyad Loutfi (undergraduate), and
8. Sankar Gopalkrishna (undergraduate).

Past members:

1. Arpan Agrawal (visiting research programmer, 2022-2024),
2. Dylan Zhang (coadvised with Maxim Raginsky, 2022-2024),
3. Thomas Reichel (masters student, class of 2024),
4. Max Fan (undergraduate, class of 2024, now at Cornell),
5. Timothy Zhou (undergraduate, class of 2024, now at UCSD),
6. Eeshan Zele (undergraduate), and
7. Zory Zhang (undergraduate).

We also welcome folks at Illinois who are super interested in proof assistants to hang out and come to lab events, chat in our Discord, and so on---let me know if this is you!

While at UW, I advised two amazing undergraduates on their own projects: Jasper Hugunin and Taylor Blau. I also mentored two fantastic students on projects related to my thesis work: RanDair Porter and Nate Yazdani. Those experiences really inspired me to become faculty!

Interested in doing research with me?

Graduate Students: I am recruiting Ph.D. students for the 2025-2026 academic year! Please apply if you are interested in making formal proof easier.

Everyone Else: I am about to go on parental leave for Spring 2024, so it is unlikely that I will take on new researchers until the 2025 academic year. If you aren't in a hurry, though, feel free to reach out!

I am the founder and president of the Computing Connections Fellowship, a fellowship that provides institution-independent transitional funding for computer science PhD students who need help escaping unhealthy environments. We are in the process of a two year pilot in the programming languages research community.

I am also the founder and previous chair of the SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M). SIGPLAN-M pairs mentors and mentees in the programming languages research community for cross-institutional mentoring relationships lasting a year by default. It currently reaches more than 200 mentors and more than 300 mentees across more than 44 countries, and has been described by mentees as "life changing" and "a career saver."

I do a lot of other leadership in the international programming languages community, as well as more traditional service. Service is a core important part of my career since it is so much bigger than my own research. My service work was formally recognized when I received the 2023 ACM SIGPLAN Distinguished Service Award. Please see my CV for more details.

In Spring 2022, I taught my new course on proof automation. I taught it again in Fall 2022. In Fall 2023, I taught CS 421 (undergraduate programming languages)! Last semester, I taught a dependent type theory reading group. I will not be teaching again until after parental leave.

I used to run competitively for Club Northwest. These days, I prefer Judo.

I have a preference for they/them pronouns, but any pronouns are OK. I am openly bisexual, and always happy to talk to LGBTQ students. I was the writer and interviewer behind The Identity Function, a blog interview series about LGBTQ computer science researchers.

I am neurodivergent, and I run a few Slack channels for neurodivergent researchers. Let me know if you're interested in joining. I am also very open about my experiences with mental illness (see, for example, my diversity statement), and very happy to talk to anyone who needs an ear. Students should keep in mind that I am a mandatory reporter by way of Title IX.

I enjoy making bagels, foraging mushrooms, studying foreign languages, playing music arcade video games, singing, writing poetry, and composing music for the piano.