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.

You can find out more about my work and vision through my Twitter megathread of ideas, my research statement, or my Ph.D. thesis. You can also check out some projects I'm currently working on.

Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-Proof Generation and Repair with Large Language Models. Under Submission. 2023.

Audrey Seo*, Chris Lam*, Dan Grossman, and Talia Ringer. Correct Compilation of Proofs About Embedded Programs. Under Submission. 2023.

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

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

Alex Sanchez-Stern*, Emily First*, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. Passport: Improving Automated Formal Verification Using Identifiers. To appear in TOPLAS. 2023.

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. To appear in Communications of the ACM (CACM). 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 wonderful collaborators at UW, UMass Amherst, Google Research, and Stanford 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 four 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? 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:

1. Cosmo Viola (Ph.D.),
2. Chris Lam (Ph.D.),
3. Hannah Leung (Ph.D., coadvised with Christopher Fletcher),
4. Dylan Zhang (Ph.D., coadvised with Maxim Raginsky),
5. Arpan Agrawal (visiting research programmer),
6. Thomas Reichel (masters student),
7. Max Fan (undergraduate),
8. Timothy Zhou (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: While I am happy to hear from potential and current graduate students who are interested, please note that I am unlikely to take on new graduate students for the 2023-2024 school year. This is just a matter of timing, and doesn't reflect on any applicants (it turns out I cannot effectively manage more than six research projects at a time). This will change in future years. If you get in touch with me, I'm still happy to try to help find good connections for you both at Illinois and at other institutions.

Undergraduate Students: I try to ensure every undergraduate student researcher has at least one graduate student researcher to work with. So my undergraduate advising capacity depends directly on my graduate students. This changes often. Feel free to ask. Right now there is a little bit of capacity, though not much. As with graduate students, I'm also happy to get you in touch with others.

Research Programmers & Postdocs: This depends a lot on funding availability. Funding for new postdocs is fairly likely for the 2023-2024 and 2024-2025 years, but it will be hard to know for sure until spring or summer 2023. Please email me if interested and I'll keep you updated.

External Collaborators: This depends a lot on alignment with student interests. Feel free to reach out! I am unlikely to enter into collaborations for which a student of mine is not directly involved, though there are some exceptions to this (like my Google visit).

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 41 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. Please see my CV for more details.

In Spring 2022, I taught my new course on proof automation. I am teaching this again in Fall 2022. Hope to see you there!

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 fine.

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 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.