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.

Dylan Zhang, Curt Tigges, Stella Biderman, Maxim Raginsky, and Talia Ringer. Can Transformers Learn to Solve Problems Recursively?. Under Submission. 2023.

Dylan Zhang, Emily First, and Talia Ringer. Getting More out of Large Language Models for Proofs. 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. To appear in ITP 2023.

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

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.

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, Stanford, 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 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),
9. Eeshan Zele (undergraduate), and
10. Sankar Gopalkrishna (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 looking to recruit a Ph.D. student for the 2024-2025 academic year! I'd particularly like to work with someone who is interested in simultaneous interactive synthesis of programs, specifications, and proofs using large language models and other tools, with an emphasis on helping users understand and debug what is synthesized. The goal is to improve the reliability of LLM-based tools for code generation by having them also synthesized proofs. Any interface built on this will account for the cognitive biases that come into play by users too, for example by providing interactive tools to help users make sense of synthesized specifications rather than naively trust them. If you're interested in programming languages, formal methods, HCI, machine learning, and NLP, this is for you! (I know that's a lot.) Feel free to reach out before applying.

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.

Research Programmers & Postdocs: This depends a lot on funding availability. Funding for new postdocs is possible 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 taught it again in Fall 2022. In Fall 2023, I'll be co-teaching CS 421 (undergraduate programming languages)!

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