Talia Ringer

For More Information

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

Education

• University of Washington, Ph.D. in Computer Science, 2021
• University of Maryland, College Park, B.S. in Mathematics and Computer Science, 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? 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.

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 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, University of Illinois, 2021-Present

Other Professional Employment

• Visiting Researcher at Google Research (N2Formal), Summer 2022 - Winter 2022
• Research Scientist Intern at Amazon (Automated Reasoning Group), Summer 2016
• Software Development Engineer II at Amazon (Amazon Business), 2012 – 2015

Professional Highlights

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

Research Interests

• 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

• 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.
• Talia Ringer. Proofs and Conversations. To appear in the AMS Early Career Notices in 2024.
• 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.
• 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.

Articles in Conference Proceedings

• Audrey Seo*, Chris Lam*, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. ITP 2024.
• 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.
• Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner*, Talia Ringer*. Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. ITP 2023.
• Emily First, Markus Rabe, Talia Ringer, Yuriy Brun. Baldur: Whole-Proof Generation and Repair with Large Language Models. ESEC/FSE 2023. Distinguished Paper Award.
• Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. Proof Repair Across Type Equivalences. PLDI 2021.
• Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. REPLICA: REPL Instrumentation for Coq Analysis . CPP 2020.
• Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. ITP 2019.
• Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting Proof Automation to Adapt Proofs. CPP 2018.
• Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, and Serdar Tasiran. A Solver-Aided Language for Test Input Generation. OOPSLA 2017.
• Talia Ringer, Dan Grossman, and Franziska Roesner. AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems. CCS 2016.

Abstracts (in print or accepted)

• Dylan Zhang, Emily First, and Talia Ringer. Getting More out of Large Language Models for Proofs. AITP 2023.
• Hannah Leung, Talia Ringer, and Christopher Fletcher. Towards Formally Verified Path ORAM in Coq. CoqPL 2023.
• Seth Poulsen, Matthew West, and Talia Ringer. Autogenerating Natural Language Proofs for Proof Education. The Coq Workshop 2022.

Pending Articles

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

Invited Lectures

• UIUC Math Colloquium
• Invited Hausdorff Special Trimester
• Invited Shonan Seminar
• Invited Dagstuhl Seminar
• Invited Panel: Career Paths
• Invited Panel: Queerness and Faculty
• Invited Panel
• Invited Panel: Human-Machine Teams for Mathematicians
• Concrete Problems in Proof Automation
• You and Your Environment
• Proof Repair Across Type Equivalences
• Proof Engineering Tools for a New Era

Other Publications

• AI-Powered Proof Generator Helps Debug Software. IEEE Spectrum article about our award-winning work on Baldur.
• Formal Verification and Deep Learning. Podcast interview for The Gradient about my work as it intersects with machine learning.
• The Thesis Review. An invited podcast interview about my thesis work and how it has informed my work since then.
• GAP Interview. An invited interview about the academic job search.
• AMA on Mentoring. An invited Ask Me Anything (AMA) session at ICFP 2021 about SIGPLAN-M.
• Proof Engineering for the People. An invited podcast interview about my work and future vision. From Building Better Systems.
• Proof Repair & Code Generation. A Galois blog post by Valentin Robert about using my tools for industrial applications.
• How Will Proof Engineering Affect the Future of Software Development? An invited podcast interview about my work and future vision. From DevDiscuss Season 6, Episode 4.

Conferences Organized or Chaired

• Beyond Bayes: Paths Towards Universal Reasoning Systems Workshop Co-Chair, ICML 2022
• Coq Workshop Co-Chair, FLoC 2022
• SPLASH Hybridization Committee, 2021
• ICFP Programming Languages Mentoring Workshop (PLMW) Co-Chair, 2020
• ICFP Mentoring Chair, 2020
• POPLmark 15 Year Retrospective Panel Lead Organizer, 2020

Other Scholarly Activities

• Journal of Automated Reasoning Reviewer, 2022
• Nature Reviewer, 2023
• POPL Program Committee, 2024
• ICFP Program Committee, 2023
• TYPES Program Committee, 2022
• ITP Program Committee, 2022
• PLDI Program Committee, 2022
• CAV Program Committee, 2021
• AIPLANS Program Committee, 2021
• HATRA Program Committee, 2020
• Mathematical Structures in Computer Science Reviewer, 2020
• CoqPL Program Committee, 2019, 2022
• CAV Artifact Evaluation Committee, 2019
• POPL Artifact Evaluation Committee, 2018, 2019

Professional Societies

• ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), Founder & Chair (2021 - 2022), Previous Chair (2023 - Present)

Service on Department Committees

• CS BPC Committee, 2022 - 2023
• CS CARES Committee, 2021 - Present

Service on College Committees

• Core Faculty Member, Grainger IDEA Institute, 2022 - Present

Service on Campus Committees

• Mental Health Ambassador

Service to Federal and State Government

• NSF Panelist, 2023
• Computational Cybersecurity in Compromised Environments (C3E) Symposium on Generative AI and Large Language Models Planning Committee, 2023
• National Academies of Science, Engineering, and Medicine AI to Assist Mathematical Reasoning Workshop Planning Committee, 2023

Other Outside Service

• Banff International Research Station (BIRS) Equity, Diversity, and Inclusion Advisory Committee, 2023-Present
• Banff International Research Station (BIRS) Scientific Advisory Committee, 2023-Present
• Computing Connections Fellowship Fund, Founder & President, 2022-Present
• ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), Mentor, 2021-Present

Research Honors

• ESEC/FSE Distinguished Paper Award 2023
• DARPA Young Faculty Award 2023
• Amazon Research Awards 2022

Public Service Honors

• ACM SIGPLAN Distinguished Service Award (June 19th, 2023 )

Improvement Activities

• Collins Scholar Program, 2022