Talia Ringer

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.

You can find out more about my work and vision through my Twitter megathread of ideas, my research statement, or my Ph.D. thesis. You can also check out some projects I'm currently working on.

Emily Ruppel*, Sihang Liu*, Elba Garza, Sukyoung Ryu, Alexandra Silva, and Talia Ringer. Long-Term Mentoring for Computer Science Researchers. Under Submission.

Alex Sanchez-Stern*, Emily First*, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. Passport: Improving Automated Formal Verification Using Identifiers. Under Submission.

Seth Poulsen, Matthew West, and Talia Ringer. Autogenerating Natural Language Proofs for Proof Education. The Coq Workshop 2022.

Talia Ringer. Proof Repair. Ph.D. Thesis, University of Washington, 2021. Defense video.

Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. Proof Repair across Type Equivalences. PLDI 2021. Talk video.

Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. REPLICA: REPL Instrumentation for Coq Analysis. CPP 2020. Talk video.

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. Errata, Q & A.

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. ITP 2019. Talk Video.

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting Proof Automation to Adapt Proofs. CPP 2018. Talk video.

Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, and Serdar Tasiran. A Solver-Aided Language for Test Input Generation. OOPSLA 2017. Talk video.

Talia Ringer, Dan Grossman, and Franziska Roesner. AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems. CCS 2016. Talk video.

I'm currently working with Emily First, Alex Sanchez-Stern, Timothy Zhou, Zhanna Kaufman, and Yuriy Brun on improving neural tactic prediction models for Coq by enriching them with missing syntactic and semantic information. The goal is use these tactic prediction models to improve performance of tools for both proof synthesis and repair. It's a lot of fun!

I'm also working with Cosmo Viola on extending proof repair tools to handle relations more general than equivalences. This is much more on the type theory side of things. I'm excited to see how powerful we can make these tools.

With Chris Lam, Audrey Seo, Dan Grossman, and Zach Tatlock, I'm working on using automation based on proof repair to automatically compile proofs about programs alongside the programs themselves---without requiring a full formal proof of compiler correctness!

With Louis Castricato, Ryan Teehan, and Shahbuland Matiana, I'm working on collecting a large pair programming dataset with atomic edits, rationales, and execution data. This is part of EleutherAI, a super cool artificial intelligence collective. So literally anyone---yes, you---can join this project if they'd like. We're in #constrastive on Discord!

I have a few other (perhaps too many) budding projects on topics like 1) formally verified secure hardware systems, and 2) the strangely rich intersection of cubical type theory and machine learning. I am always happy to hear what students want to work on!

I'm fortunate to advise four wonderful students at UIUC, as part of the Illinois Theorem Provers (ITP) lab (huge credit to Yao Li for the name), part of the PL/FM/SE group:

1. Cosmo Viola (Ph.D.),
2. Chris Lam (Ph.D.),
3. Thomas Reichel (masters student), and
4. Timothy Zhou (undergraduate).

I'm excited to advise two new students starting next year:

1. Hannah Leung (Ph.D., coadvised with Christopher Fletcher), and
2. Shizhuo Zhang (Ph.D., coadvised with Maxim Raginsky).

I'm also lucky to get to work with some wonderful external students---like, a lot of wonderful external students, because I find collaboration way too much fun for my own good. Honestly I couldn't maintain this list. But they're all great I promise.

While at UW, I advised two amazing undergraduates on their own projects: Jasper Hugunin and Taylor Blau. I also mentored two fantastic students on projects related to my thesis work: RanDair Porter and Nate Yazdani. Those experiences really inspired me to become faculty!

I am the founder and president of the Computing Connections Fellowship, a fellowship that provides institution-independent transitional funding for computer science PhD students who need help escaping unhealthy environments. We are in the process of a two year pilot in the programming languages research community.

I am also the founder and chair of the SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M). SIGPLAN-M pairs mentors and mentees in the programming languages research community for cross-institutional mentoring relationships lasting a year by default. It currently reaches more than 200 mentors and more than 300 mentees across more than 41 countries, and has been described by mentees as "life changing" and "a career saver."

I do a lot of other leadership in the international programming languages community, as well as more traditional service. Please see my CV for more details.

In Spring 2022, I taught my new course on proof automation. I will be teaching this again in Fall 2022. Hope to see you there!

I am a competitive runner. I used to run for Club Northwest.

I have a weak preference for they/them pronouns, but any pronouns are fine. Here is a quick FAQ about my relationship with gender.

I am openly bisexual, and always happy to talk to LGBTQ students. I was the writer and interviewer behind The Identity Function, a blog interview series about LGBTQ computer science researchers.

I am very open about my experiences with mental illness (see, for example, my diversity statement), and very happy to talk to anyone who needs an ear. Students should keep in mind that I am a mandatory reporter by way of Title IX.

I enjoy making bagels, foraging mushrooms, studying foreign languages, playing music arcade video games, singing, writing poetry, and composing music for the piano.