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.

I am hiring Ph.D. students! Please contact me if you are interested. 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. Work with me!

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.

Finally, 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!

I have a few other budding projects, and I am always happy to hear what students want to work on!

I'm fortunate to advise three wonderful students at UIUC:

1. Cosmo Viola (Ph.D.),
2. Chris Lam (Ph.D.), and
3. Timothy Zhou (undergraduate).

I'm also lucky to get to work with three external students:

1. Emily First (Ph.D., UMass Amherst),
2. Zhanna Kaufman (Ph.D., UMass Amherst), and
3. Audrey Seo (Ph.D., UW).

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!

In Spring 2022, I'm super excited to teach my new course on proof automation. Hope to see you there!

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

I am the founder and chair of SIGPLAN-M, an international long-term mentoring program for aspiring and current programming languages researchers.

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 once I am a mandatory reporter.

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