For more information
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 openly bisexual, and 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).
- 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.
Articles in Conference Proceedings
- 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.
- 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
- ICFP Mentoring Chair, 2020
- ICFP Programming Languages Mentoring Workshop (PLMW) Co-Chair, 2020
- SPLASH Hybridization Committee, 2021
- Coq Workshop Co-Chair, 2022
Other Scholarly Activities
- CAV Program Committee, 2021
- PLDI Program Committee, 2022
- ITP Program Committee, 2022
- ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), Founder & Chair, 2021 - 2022
Service on Department Committees
- CS CARES Committee, 2021-2022
Other Outside Service
- ACM SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), Mentor, 2021-2022
Recent Courses Taught
- CS 598 TLR - Proof Automation