Talia Ringer

Professor, PL/FM/SE at UIUC. Proof automation. SIGPLAN-M Founder, CCF President. They/them, ND, bi.

website: https://dependenttyp.es

Last Notes

2026-07-13 15:44:01 UTC

- reply

Though you are probably making it into a conflict now...

2026-07-13 15:43:46 UTC

- reply

talk to the PC chair probably, IDK if that is a conflict, I know it is not against policy to post links to preprints of papers to share research findings unless you say where you submitted it to

2026-07-13 15:30:56 UTC

Some of my awesome Ph.D. students and collaborators helped me finally understand what on earth I was doing in my Ph.D. thesis work in a way that is precise and generalizable. Like, they turned my vibes into a formalization. Just so excited about this
https://trey3p.github.io/papers/prt.pdf

2026-06-10 17:59:01 UTC

Need a running example for my NSF CAREER. Would appreciate some help since I suck at examples, but having one would make my proposal way better.
It should be a verification or formal math project (described at a very high level, like "suppose we are verifying a compiler from our own language to CompCert CLight" or whatever) with the following (IME very common) properties:
1. It is well-motivated and based on actual proof developments I can cite.
2.I can simplify it dramatically when discussing it in the proposal for exemplary purposes.
3. The programs, definitions, and theorem statements are not all known in advance---it makes sense for the proof engineer to figure those things out as they go.
4. It depends on a custom library and/or exists in a specific domain that uses a lot of custom definitions and custom styles (but not a monorepo like mathlib).
5. It is something that it would make sense to collaborate on with a sizable group of collaborators, who may be opinionated about questions of proof engineering best practices, or about best practices specific to that domain.
Please let me know if you have ideas. Can be in any proof assistant language.

2026-06-09 12:06:25 UTC

- reply

the one I shared is a gift article since I am a subscriber, should also be free

2026-06-09 00:02:29 UTC

Neat to see this article come out as I'm navigating fears of this in the Agda community
https://www.nytimes.com/2026/06/08/science/ai-scoop-young-mathematicians.html?unlocked_article_code=1.olA.dJte.wZXzslO706sU&smid=url-share

2026-02-12 01:38:58 UTC

- reply

it's very modern stuff

2026-02-12 01:37:22 UTC

- reply

https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf

2026-02-12 01:27:10 UTC

- reply

Hilbert seems to strike an unhappy medium. E is meant to mirror Euclid's proofs very closely, so usability should be at the forefront, but the axiom set is quite large (thankfully the metatheory is well understood though). The student prototype however used a small DTT kernel, then some internal kernel axioms on top of that to model E

2026-02-12 01:24:18 UTC

- reply

Tarski actually has a lot of appeal as a kernel too IMO (really small axiom set, decidable proof search) but students felt the axiom set was so, so low-level that it was too hard to build the infrastructure needed to have good usability on top of that

2026-02-12 01:22:24 UTC

- reply

The work these students did in two weeks of class was genuinely impressive. Can't wait to see what our proof assistant is like in the end

2026-02-12 01:21:20 UTC

The three different Euclidean geometric kernel prototypes are done. Now it is time for the class to converge on one foundations and write our final kernel. It's looking like E over Tarski and Hilbert. But jury is still out on TT vs. logic, and on LCF vs. de Bruijn

2024-10-06 13:24:36 UTC

Hey guys. Our beautiful daughter Sarah Rose El-Kebir was in a hurry to get out and did not want to wait five more weeks. So she entered the world on Friday morning. She's doing well and I'm doing well. She's small and needs a bit of extra help, so I'm in and out of the NICU for now. But she's very strong and she's doing great in there. Mohammed and I are very in love with her. Feel free to DM for cute baby pics if we know each other personally.

2024-09-15 17:08:53 UTC

What are some domain-specific program logics people know about? Particularly interested in domains where it's not obvious that the thing being reasoned about is a "program," but it can in fact be viewed as such, and so a logic can be built around it.