Max Willsey's Avatar

Max Willsey

@mwillsey.com

https://mwillsey.com asst prof @ uc berkeley eecs mastodon: @mwillsey@discuss.systems

500
Followers
108
Following
13
Posts
11.05.2023
Joined
Posts Following

Latest posts by Max Willsey @mwillsey.com

Equality reasoning in Vampire The EGRAPHS community discusses e-graphs and related technologies for program optimization, verification, and synthesis.

This week at the EGRAPHS Seminar, Marton Hajdu from the Vampire team will present his work on equality reasoning in the Vampire tool. Join us!

Thursday 2/19, 9AM PT on Zoom
Recordings on youtube after

egraphs.org/meeting/2026...

17.02.2026 16:10 πŸ‘ 7 πŸ” 0 πŸ’¬ 0 πŸ“Œ 0
Post image

OAKLAND WE DID IT!!!! πŸ†

22.09.2025 04:45 πŸ‘ 192 πŸ” 62 πŸ’¬ 3 πŸ“Œ 14
grind in Lean 4 The EGRAPHS community discusses e-graphs and related technologies for program optimization, verification, and synthesis.

In this month's EGRAPHS Community Meeting, Leo de Moura will present on the internals of the `grind` tactic in Lean 4.

Join us on Zoom 9am PT this Thursday (9/18). Or catch the recording after!

egraphs.org/meeting/2025...

16.09.2025 16:16 πŸ‘ 4 πŸ” 0 πŸ’¬ 0 πŸ“Œ 0

I had a great time at Kris's workshop in May! Lots of inspiring talks and discussions. He has posted a mega-video of all the recorded talks, I highly recommend checking some of them out if you're into Datalog, logic programming, or incrementalization. There is even some e-graph stuff in there!

08.07.2025 16:50 πŸ‘ 11 πŸ” 2 πŸ’¬ 0 πŸ“Œ 0

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: www.mwillsey.com/blog/pldi-2025

16.06.2025 00:38 πŸ‘ 13 πŸ” 0 πŸ’¬ 0 πŸ“Œ 0
Counting - The Little Book of Rust Macros

Idk about tiple dot access. You can count in a few ugly ways: lukaswirth.dev/tlborm/decl-....

Tuple unpacking is a little neater.

05.06.2025 13:46 πŸ‘ 1 πŸ” 0 πŸ’¬ 1 πŸ“Œ 0
Preview
EGRAPHS 2025 - PLDI 2025 Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via eq...

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: pldi25.sigplan.org/home/egraphs...

24.03.2025 16:32 πŸ‘ 10 πŸ” 3 πŸ’¬ 0 πŸ“Œ 0
Slotted E-Graphs The EGRAPHS community discusses e-graphs and related technologies for program optimization, verification, and synthesis.

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!

egraphs.org/meeting/2025...

17.03.2025 16:21 πŸ‘ 2 πŸ” 2 πŸ’¬ 0 πŸ“Œ 0

Very excited that egg was picked as SIGPLAN research highlight!! Thanks to all my awesome co-authors!

01.03.2025 02:44 πŸ‘ 7 πŸ” 0 πŸ’¬ 0 πŸ“Œ 0
C.C. Lemma: induction and lemma discovery in e-graphs The EGRAPHS community discusses e-graphs and related technologies for program optimization, verification, and synthesis.

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.

egraphs.org/meeting/2025...

18.02.2025 17:17 πŸ‘ 4 πŸ” 1 πŸ’¬ 0 πŸ“Œ 0
A screenshot of YJIT latency over time, showing that p99 latency stays lower than MRI even during deployments.

A screenshot of YJIT latency over time, showing that p99 latency stays lower than MRI even during deployments.

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

22.01.2025 03:18 πŸ‘ 56 πŸ” 16 πŸ’¬ 1 πŸ“Œ 1
EGRAPHS 2025 - PLDI 2025 Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via eq...

The EGRAPHS workshop brings together researchers and practitioners that use e-graphs and related techniques. The paper submission deadline is on April 17. More info can be found here: pldi25.sigplan.org/home/egraphs... and egraphs.org

07.02.2025 00:26 πŸ‘ 0 πŸ” 2 πŸ’¬ 2 πŸ“Œ 0

HYTRADBOI was the best bang-for-my-buck (both in time and money) event that I attended last year. This year looks equally great! If you are interested in PL or DB, it's worth it; if you like both it's a must see!

Sidenote: I think it's a great example of how to run an efficient remote conference!

01.02.2025 16:57 πŸ‘ 5 πŸ” 1 πŸ’¬ 0 πŸ“Œ 0
LATTE ’25

β˜•οΈ We’re running LATTE again: our ASPLOS workshop about languages/compilers/tools/whatever for hardware design.

Submissions are just little 2-pagers, due on January 31. Plenty of time to throw something together! capra.cs.cornell.edu/latte25/

09.01.2025 17:15 πŸ‘ 23 πŸ” 10 πŸ’¬ 0 πŸ“Œ 0

It's 2025, which means PLISS is this year... May to be specific! If you're interested in studying programming language implementations, please make sure to express your interest in time pliss.org/2025/

06.01.2025 18:57 πŸ‘ 25 πŸ” 19 πŸ’¬ 0 πŸ“Œ 0

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 @samps.phd for the Bril infrastructure!

Some students have opted to make their final projects public on the course site, so check them out!

github.com/mwillsey/cs2...

27.12.2024 02:10 πŸ‘ 12 πŸ” 1 πŸ’¬ 0 πŸ“Œ 0
Home Β· SoCal PLS

SoCal Programming Languages and Systems is back and will be @ucsd_cse in February!
Submit your abstracts!
socalpls.github.io

@ranjitjhala.bsky.social @manu.sridharan.net @cristalopes.bsky.social
Reposts appreciated!

20.12.2024 19:50 πŸ‘ 24 πŸ” 11 πŸ’¬ 2 πŸ“Œ 1
EGRAPHS 2025 - PLDI 2025 Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via eq...

The fourth (!!) EGRAPHS Workshop will take place in June at PLDI 2025 in Seoul!

pldi25.sigplan.org/home/egraphs...

More details to come later, but start thinking about your submission :)

29.11.2024 14:35 πŸ‘ 16 πŸ” 4 πŸ’¬ 0 πŸ“Œ 0

NES emulator is a fun one!

28.11.2024 19:59 πŸ‘ 3 πŸ” 0 πŸ’¬ 0 πŸ“Œ 0
Preview
Ground Lambda Prolog Today, I thought today I’d be writing a lambda prolog interpreter. While trying to explain what it’s doing, I got kind of mired in some other interesting ideas.

[New Blog Post] Ground Lambda Prolog www.philipzucker.com/ground_lambd...

26.11.2024 01:01 πŸ‘ 6 πŸ” 1 πŸ’¬ 0 πŸ“Œ 1