For More Information
- University of Washington, Ph.D. in Computer Science, 2021
- University of Maryland, College Park, B.S. in Mathematics and Computer Science, 2012
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).
- 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
- 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.
- Dependent Type Theory
- Interactive Theorem Proving
- Proof Automation
- Proof Engineering
- 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
- 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
- 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.
- 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.
- Cosmo Viola, Max Fan, and Talia Ringer. Towards Proof Repair in Cubical Agda. 2023.
- Dylan Zhang, Curt Tigges, Stella Biderman, Maxim Raginsky, and Talia Ringer. Can Transformers Learn to Solve Problems Recursively? Under Submission. 2023.
- Audrey Seo*, Chris Lam*, Dan Grossman, and Talia Ringer. Correctly Compiling Proofs About Programs Without Proving Compilers Correct. Under Submission. 2023.
- 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
- 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
- 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
- DARPA Young Faculty Award 2023
- Amazon Research Awards 2022
Public Service Honors
- ACM SIGPLAN Distinguished Service Award (June 19th, 2023 )
- Collins Scholar Program, 2022
Recent Courses Taught
- CS 421 - Progrmg Languages & Compilers
- CS 576 - Topics in Automated Deduction
- CS 598 TLR - Proof Automation