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 Types
- 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.
- ACM SIGPLAN Long-Term Mentoring Committee: Founder & Chair