May 25-27, 2025, I hosted an event, the "Minnowbrook Logic Programming Seminar," in Blue Mountain Lake, NY. I recorded 11 talks on Datalog-related interests, totaling over 9+ hours of video, which I have just now published on YouTube https://youtu.be/3ec9VfMUVa8

I'm at PLDI 2025 right now! Come say hi if you are too :)

Lots of cool e-graph stuff happening this week: the egglog tutorial, the EGRAPHS workshop, and some excited papers. I'm trying to collect it all here: https://www.mwillsey.com/blog/pldi-2025

@j2kun @regehr Other folks have covered this pretty well! Basically, egg-style search and saturate is far too expensive for most general purpose compilers. It has found some use in domain specific situations, or when smart people like @cfallin go make their own version specialized to their performance needs!

So who does e-graphs for equality saturation in a real compiler? I want to hear about performance impact both to the compiler and the resulting program. @regehr maybe?

@sandmouth @krismicinski @rntz I was looking at the grind tactic the other day as well. Seems like it’s very much in the style of the “Efficient E-matching” paper, and so is Z3. Definitely egraphs going on in there!

@rntz @nick you changed from strings with prefix to sets with inclusion. In in your order, f “b” would have to wait, since they are compatible. I agree it’s not super intuitive when the patterns can overlap in that sense. But consider having a wildcard pattern pattern at the end of your match: very typical, pretty intuitive, and obviously overlapping. I guess it remains to show the utility of first-match for overlapping, non-bottom pattern.

@nick @rntz ah yes, since the whole point is that arm order matters, the last arm should be privileged to not worry about incompatibility as long as the scrutinee >= pattern.

@nick @rntz

Maybe another way to think about it is that incompatibility gives you a way to state a sensible semantics for first-wins.

Consider strings with prefix order: a < ab < abc, and abc |/| abd.

And consider the program:
match x { "ab" -> ... | "abc" -> ... }

To achieve first match semantics, one implementation would be:

- compare incoming x to "ab":
- if x >= "ab", fire that arm
- elseif x || "ab", wait
- else, it must be that x |/| "ab", so you can move on from this arm.

Indeed in this example, the second arm will never fire in match-first semantics. So perhaps the other ordering is more interesting. Either way, this semantics means that you have a monotone output stream because only one match arm will ever fire.

This is going to be so much fun. "Program Optimisation with E-Graphs", a Dagstuhl workshop organised by @mwillsey, @cfallin, @michel and me. Max has done a fantastic job driving this proposal. It will be great to be back at Dagstuhl again.
https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/26022

It's that time of year! The submission site for the EGRAPHS Workshop is open!

We welcome talk proposals on published work, in-progress work, real-world applications, and anything in between. Get your 2-6 page abstract in by **April 17 AoE**!

More details here: https://pldi25.sigplan.org/home/egraphs-2025

This month's EGRAPHS seminar is on Slotted E-Graphs! The authors will be presenting on new ways to add support for binders to e-graphs.

This Thursday, 9am PT on Zoom!

https://egraphs.org/meeting/2025-03-20-slotted

The EGRAPHS seminar series resumes Thursday 9am PT on Zoom! See you all there.

Cole Kurashige will be presenting on C.C. Lemma, a prover featuring induction and lemma discovery in e-graphs.

https://egraphs.org/meeting/2025-02-20-cc-lemma

The first few HYTRADBOI 2025 talks are ready! I'm so excited to be finally able to tell people about them!

Talk #1: A YJIT interview with Maxime Chevalier-Boisvert

If you like PL or DB, you should check out HYTRADBOI! If you like both, it really is a must see.

https://www.hytradboi.com/2025

The program is up and tickets are live at https://www.hytradboi.com/2025/#program.

I'll keep updating this thread as the last 10 talks hit camera-ready.

@rntz 🇺🇸🫡

Just wrapped up grading for grad compilers! It was a ton of fun, and I hope to keep iterating and improving the course! hat tip to @adrian for the Bril infrastructure which I (ab)used for this course!

Some students have opted to make their final projects public on the course website, so check them out! I know some of them are looking for compilers jobs, so if you're looking for compilers people, check here!

https://github.com/mwillsey/cs265/blob/2024-fall/project.md#public-projects

BART is *not playing* with this new page on the fiscal cliff https://www.bart.gov/about/financials/crisis

@regehr Interesting! The link you shared mentioned that LLVM considers natural loops to be the _maximal_ set of nodes that fit the usual definition (connected, only reachable thru header, etc). Other resources I looked at define it to be the smallest such set, which would mean the picture includes two loops, one for each backedge.

@regehr Does LLVM consider this one loop or two?