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-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.