Talia Ringer

For More Information

• Talia Ringer's GitHub
• Talia Ringer's website

Education

• Ph.D., Computer Science, University of Washington, 2021
• B.S., Mathematics and Computer Science, University of Maryland, College Park, 2012

Biography

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? A world in which mathematicians, both amateur and professional, can seamlessly collaborate with one another at a massive scale without compromising correctness? 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 machine learning---all in service of real humans.

Prior to Illinois, I earned my PhD in 2021 from the University of Washington, working with the wonderful PLSE group. Prior to graduate school, I earned my BS in Computer Science and Mathematics from the University of Maryland, then worked as a software engineer at Amazon for three years.

I am extremely passionate about building a welcoming environment for students. I am founder and chair of the SIGPLAN long-term mentoring committee (called SIGPLAN-M), an international long-term cross-institutional mentoring program for aspiring and current programming languages researchers spanning dozens of countries and reaching hundreds of mentees around the world. I am also the founder and president of the Computing Connections Fellowship, a fellowship that provides institution-independent transitional funding for computer science Ph.D. students who need help escaping unhealthy environments.

I am openly bisexual and prefer they/them pronouns; I am always happy to talk to LGBTQ students. I am neurodivergent and happy to talk about my ADHD. I am also very open about my experiences with mental illness, and very happy to talk to anyone who needs an ear (though students should keep in mind that I am a mandatory reporter through Title IX).

Academic Positions

• Assistant Professor, Siebel School of Computing and Data Science, University of Illinois Urbana-Champaign, 2021-Present

Other Professional Employment

• Visiting Researcher, Google Research (N2Formal), Mountain View CA, Summer 2022 - Winter 2022
• Research Scientist Intern, Automated Reasoning Group, Amazon, New York NY, Summer 2016
• Software Development Engineer II, Amazon, Seattle WA, 2015

Professional Highlights

• My work founding SIGPLAN-M and CCF (along with my other service work) led me to receive the 2023 ACM SIGPLAN Distinguished Service Award.
• Proof repair, the subject of my PhD thesis, has since been reimplemented by researchers and engineers at Amazon and NASA, and adapted to the languages they use. It is also the subject of a DARPA AI Exploration called PEARLS, a grant for which I am primary PI.

Other Undergraduate Advising Activities

• Eyad Loutfi, Senior Thesis: Adding new automation to proof repair, SSCDS, University of Illinois Urbana-Champaign, 2024-2025.
• Zory Zhang, Senior Thesis: Learning structurally recursive functions, Computer Science, University of Illinois Urbana-Champaign, 2023.
• Sankar Gopalkrishna (coadvised with Christopher Fletcher and Hannah Leung), Senior Thesis: Verified secure computer architectures, Computer Science, University of Illinois Urbana-Champaign, 2022-2025.
• Eeshan Zele (coadvised with Christopher Fletcher and Hannah Leung), Senior Thesis: Verified secure computer architectures, Computer Science, University of Illinois Urbana-Champaign, 2022-2024.
• Max Fan, Senior Thesis: Building practical proof repair tools for relations more general than type equivalences, Placement: Ph.D at Cornell, Computer Science, University of Illinois Urbana-Champaign, 2022-2024.
• Timothy Zhou, Senior Thesis: Improving neural tactic prediction models for proof synthesis and repair, Placement: Ph.D. at UCSD, Computer Science, University of Illinois Urbana-Champaign, 2021-2024.
• Jasper Hugunin (coadvised with Dan Grossman), Senior Thesis: Constructing Inductive-Inductive Types in Cubical Type Theory (published in FOSSACS 2019), University of Washington, 2018-2019.
• Taylor Blau (coadvised with Dan Grossman), Senior Thesis: Verifying Strong Eventual Consistency in δ-CRDTs, University of Washington, 2019-2020.

Research Interests

• Formal Mathematics
• Dependent Type Theory
• Verification
• Interactive Theorem Proving
• Proof Automation
• Proof Engineering

Monographs

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

Selected Articles in Journals

• Cosmo Viola, Max Fan, and Talia Ringer. "Proof Repair across Quotient Type Equivalences," Proceedings of the ACM on Programming Languages (PACMPL), Vol. 9, Issue: OOPSLA, Article No. 386, pp. 3177-3202, 2025.
• Borhane Blili-Hamelin, Christopher Graziul, Leif Hancox-Li, Hananel Hazan, El-Mahdi El-Mhamdi, Avijit Ghosh, Katherine Heller, Jacob Metcalf, Fabricio Murai, Eryk Salvaggio, Andrew Smart, Todd Snider, Mariame Tighanimine, Talia Ringer, Margaret Mitchell, and Shiri Dori-Hacohen. "Position: Stop Treating ‘AGI’ as the North-Star Goal of AI Research," (Position Track), Proceedings of Machine Learning Research (PMLR), Vol. 235 (ICML), pp. 1-25, 2025.
• 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." Transactions on Machine Learning Research (TMLR), July Issue, pp. 1-30, 2024.
• Emily First, Markus Rabe, Talia Ringer, Yuriy Brun. "Baldur: Whole-Proof Generation and Repair with Large Language Models," Proceedings of the ACM on Software Engineering (PACMSE), Vol. 1, Issue: FSE, Article No. 7, pp. 122-145, 2023.
• Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. "Passport: Improving Automated Formal Verification Using Identifiers." ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 45, Issue 2, Article No. 12, pp 1-30, 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), Vol. 66, Issue 5, pp 33-35, 2023.
• Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, and Serdar Tasiran. "A Solver-Aided Language for Test Input Generation," Proceedings of the ACM on Programming Languages (PACMPL), Vol. 1, Issue: OOPSLA, Article No. 91, pp. 1-25, 2017.

Articles in Conference Proceedings

• Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, and Emily First. "Cobblestone: Iterative Automation for Formal Verification," (Research Track), Proceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE), pp. 1-13, 2026. (Acceptance Rate: 21.8%)
• Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang, Talia Ringer, and Yuriy Brun. "QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning," (Research Track), Proceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE), pp. 1-13, 2025. (Acceptance Rate: 14.9%)
• Audrey Seo, Chris Lam, Dan Grossman, and Talia Ringer. "Correctly Compiling Proofs About Programs Without Proving Compilers Correct," Proceedings of the 15th International Conference on Interactive Theorem Proving (ITP), Series: Leibniz International Proceedings in Informatics (LIPIcs), Vol. 309, pp. 29:1-29:20, 2024. (Acceptance Rate: 54.9%)
• Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, and Yuriy Brun. "Proofster: Automated Formal Verification," (Demo Track), 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pp. 13-16, 2023. (Acceptance Rate: 35.7%)
• Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. "Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset," Proceedings of the 14th International Conference on Interactive Theorem Proving (ITP), Vol. 268 [2], pp. 27:1-27:18, 2023. (Acceptance Rate: 46.2%)
• Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. "Proof Repair Across Type Equivalences," Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (PLDI), pp. 112-127, 2021. (Acceptance Rate: 22%)
• Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. "REPLICA: REPL Instrumentation for Coq Analysis," Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 99-113, 2020. (Acceptance Rate: 31%)
• Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. "Ornaments for Proof Reuse in Coq," Proceedings of the 10th International Conference on Interactive Theorem Proving (ITP), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 141, pp. 26:1-26:19, 2019. (Acceptance Rate: 28%)
• Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. "Adapting Proof Automation to Adapt Proofs," Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 115-129, 2018. (Acceptance Rate: 48.6%)
• Talia Ringer, Dan Grossman, and Franziska Roesner. "AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems," ACM Conference on Computer and Communications Security (CCS), pp. 204-216, 2016. (Acceptance Rate: 16.5%)

Abstracts (in print or accepted)

• Tom Reichel and Talia Ringer. "ProofDB: A Prototype Natural Language Coq Search Engine." Conference on Artificial Intelligence and Theorem Proving (AITP), 2024.
• Dylan Zhang, Emily First, and Talia Ringer. "Getting More out of Large Language Models for Proofs," Conference on Artificial Intelligence and Theorem Proving (AITP), 2023.
• Hannah Leung, Talia Ringer, and Christopher Fletcher. "Towards Formally Verified Path ORAM in Coq," International Workshop on Coq for Programming Languages (CoqPL), 2023.
• Seth Poulsen, Matthew West, and Talia Ringer. "Autogenerating Natural Language Proofs for Proof Education," The Coq Workshop, 2022.

Pending Articles

• Jilin Hu, Jianyu Zhang, Yongwang Zhao, and Talia Ringer. "HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement,"  Under Submission, 2025.

Invited Lectures

• Big Proof
• Big, Pretty Math
• Bridging Neural and Symbolic Proof Automation
• Language Models for Formal Proof
• Proofs and Conversations
• Language Models for Formal Proof
• Invited Participant
• Mostly Automated Proof Repair for Verified Libraries
• Panel: Career Paths
• Panel Discussion: Toward Human-Level Mathematical Reasoning
• Panel: Faculty and Queerness
• Panel: Human-Machine Teams for Mathematicians
• Concrete Problems in Proof Automation
• You and Your Environment
• Proof Repair Across Type Equivalences
• Proof Repair Across Type Equivalences

Bulletins

• Talia Ringer. "Mathematicians put AI model AlphaProof to the test," Nature, Section: News & Views, Vol. 647, Issue 8089, pp. 29-30, November 12, 2025.
• Guest, "AI Through the Lens of Journalism," Radio Show: The 21st Show, Illinois Public Media, August 27, 2025.
• Talia Ringer. "Proofs and Conversations," Notices of the American Mathematical Society, Vol. 71, Issue 9, Section: Early Career, pp. 1276-1279, October 2024.
• Guest, "Talia Ringer: Formal Verification and Deep Learning," The Gradient Podcast hosted by Daniel Bashir, May 25, 2023.
• Guest, "[41] Talia Ringer - Proof Repair," The Thesis Review, Episode No: 41, March 30, 2022.
• Guest, "Proof Engineering for the People," Podcast Series: Building Better Systems, Episode 13, July 26, 2021.
• Guest, "Getting Academic Positions (GAP) Interviewing Series," Podcast hosted by Manuel Rigger, July 21, 2021.
• Guest, Ask Me Anything (AMA) Session, ICFP, August, 26, 2021.
• Guest, "How Will Proof Engineering Affect the Future of Software Development?" Podcast Series: DevDiscuss, Season 6, Episode 4, June 15, 2021.
• Reference to Research on Tools for Industrial Applications, "Proof Repair & Code Generation," A Galois blog post by Valentin Robert, April 20, 2021.

Magazine Articles

• Reference to Distinguished Paper Award at ESEC/FSE, "AI-Powered Proof Generator Helps Debug Software," IEEE Spectrum, Vol. 61, Issue 3, pp. 10-11, January 25, 2024.

Journal Editorships

• Peer Reviewer, Nature, 2025
• Peer Reviewer, Nature, 2023
• Peer Reviewer, Journal of Automated Reasoning (JAR), 2022
• Peer Reviewer, Mathematical Structures in Computer Science (MSCS), 2020

Conferences Organized or Chaired

• General Chair, 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2026
• Co-Chair, Coq Workshop, Federated Logic Conference (FLoC), 2022
• Co-Chair, Beyond Bayes: Paths Towards Universal Reasoning Systems Workshop, International Conference on Machine Learning (ICML), 2022
• Mentoring Chair, International Conference on Functional Programming (ICFP), 2020
• Co-Chair, Programming Languages Mentoring Workshop (PLMW), International Conference on Functional Programming (ICFP), 2020

Professional Societies

• Program Committee, International Conference on Interactive Theorem Proving (ITP), 2026
• Program Committee, Programming Language Design and Implementation (PLDI), 2026
• Program Committee, International Conference on Certified Programs and Proofs (CPP), 2026
• Selection Committee, ACM SIGPLAN Distinguished Service Award Committee, 2025 - Present
• Program Committee, ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2024
• Previous Chair, ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), 2023 - Present
• Program Committee, International Conference on Functional Programming (ICFP), 2023
• Program Committee, International Conference on Interactive Theorem Proving (ITP), 2022
• Program Committee, Programming Language Design and Implementation (PLDI), 2022
• Mentor, ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), 2021-Present
• Founder & Chair, ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), 2021 - 2022
• Hybridization Committee, Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) Conference, 2021
• Panel Organizer, POPLmark 15 Year Retrospective, Principles of Programming Languages (POPL), 2020
• Artifact Evaluation Committee (AEC), Computer-Aided Verification (CAV), 2019
• Artifact Evaluation Committee (AEC), Principles of Programming Languages (POPL), 2019
• Artifact Evaluation Committee (AEC), Principles of Programming Languages (POPL), 2018

Service on Department Committees

• Member, BPC Committee, Computer Science, University of Illinois Urbana-Champaign, 2022 - 2023
• Member, CS CARES Committee, SSCDS, University of Illinois Urbana-Champaign, 2021 - Present

Service on College Committees

• Core Faculty Member, Grainger College of Engineering IDEA Institute, 2022-2024

Service on Campus Committees

• Mental Health Ambassador, University of Illinois Urbana-Champaign, 2021 - Present

Service to Federal and State Government

• Panelist, National Science Foundation, 2024
• Panelist, National Science Foundation, 2023
• Scientific Advisory Committee, Banff International Research Station (BIRS), 2023-Present
• Equity, Diversity, and Inclusion Advisory Committee, Banff International Research Station (BIRS), 2023-Present
• Planning Committee, Computational Cybersecurity in Compromised Environments (C3E) Symposium on Generative AI and Large Language Models, 2023
• Planning Committee, AI to Assist Mathematical Reasoning Workshop, National Academies of Science, Engineering, and Medicine (NASEM), 2023

Other Outside Service

• Program Committee, International Workshop on Rocq for Programming Languages (RocqPL), 2026
• Program Committee, International Workshop on Coq for Programming Languages (CoqPL), 2023
• Founder & President, Computing Connections Fellowship Fund, 2022-2025
• Program Committee, International Workshop on Coq for Programming Languages (CoqPL), 2022
• Program Committee, International Conference on Types for Proofs and Programs (TYPES), 2022
• Program Committee, Computer-Aided Verification (CAV), 2021
• Program Chair, Artificial Intelligence for Programming Language and Software Engineering (AIPLANS) Workshop, 2021
• Program Committee, Workshop on Human Aspects of Types of Reasoning Assistants (HATRA), 2020
• Program Committee, International Workshop on Coq for Programming Languages (CoqPL), 2019

Honors

• ACM SIGSOFT Distinguished Paper Award, ESEC/FSE, 2023
• Young Faculty Award, Defense Advanced Research Projects Agency (DARPA), 2023
• ACM SIGPLAN Distinguished Service Award, 2023 (June 19th, 2023 )
• Recipient, Amazon Research Awards, 2022

Improvement Activities

• Collins Scholar Program, Academy for Excellence in Engineering Education (AE3), Grainger College of Engineering, Illinois, 2022