Max Willsey
where else to find them
website:https://mwillsey.com
github:mwillsey
bluesky:mwillsey.com
mastodon:@mwillsey@discuss.systems
x:mwillsey
what they talk about
all 5 in the filters
where they keep going back
- POPL3 editions2021–2023
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2026
- OOPSLA2 editions2021–2023
all 6 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Zachary Tatlock11 talks
- Yisu Remy Wang5 talks
- Oliver Flatt4 talks
- Chandrakana Nandi9 talks
- David Cao3 talks
- Amy Zhu3 talks
| title | conference | date |
|---|---|---|
| Navigating AND–OR Graph Modifications to Debug Failing Proof Search | PLDI 2026 | 2026-06-15 |
Provides a concrete debugging method that navigates modifications to AND–OR graphs rather than the raw graph, implemented by compiling modification constraints… | ||
| Optimism in Equality Saturation | PLDI 2026 | 2026-06-15 |
Shows that a naive optimistic e-class analysis on e-graphs becomes unsound because rewrites create ill‑formed cycles that look like loops but aren’t, and… | ||
| Panel: Compilation Frameworks | Sparse 2024 | 2024-06-25 |
Discussion shows a concrete path for quantify over bitwidth proofs: Lean supports quantifying bitwidth but only offers high‑performance automation for fixed… | ||
| Equality Saturation and Joins | Sparse 2024 | 2024-06-25 |
Equality saturation uses egraphs to represent many equivalent programs and extraction picks the cheapest term after saturating rewrites. A relational encoding… | ||
| A Tour of Program Optimization | PLMW@PLDI 2024 | 2024-06-24 |
Presents a concrete taxonomy: program optimization splits into transformation (term rewriting, local rewrites, termination and confluence proofs) and synthesis… | ||
| Datalog and Equality Saturation | Logic and Algebra for Query Evaluation 2023 | 2023-11-13 |
Claims that equality saturation can be encoded as Datalog while keeping the congruence closure algorithm work in practice lead to a concrete system and… | ||
| Equality Saturation Theory Exploration à la Carte | OOPSLA 2023 | 2023-10-23 |
Enumo is a domain-specific language for programmable theory exploration that gives users small, composable operators to guide automatic inference of rewrite… | ||
| Better Together: Unifying Datalog and Equality Saturation | PLDI 2023 | 2023-06-17 |
egglog claims a single system that combines Datalog-style declarative analyses with equality-saturation rewriting by introducing functional dependency repair… | ||
| babble: Learning Better Abstractions with E-Graphs and Anti-unification | POPL 2023 | 2023-01-15 |
Presents Library Learning Modulo Theory (LLMT) implemented as the tool babble, which uses e-graphs plus a new e-graph anti-unification algorithm and targeted… | ||
| Relational E-matching | POPL 2022 | 2022-01-16 |
Transforms e-graphs into relational tables and patterns into conjunctive queries, then runs worst-case optimal joins (generic join) to guarantee asymptotic… | ||
| Rewrite Rule Inference Using Equality Saturation | OOPSLA 2021 | 2021-10-17 |
Describes a system called Ruler that uses equality saturation over e-graphs to infer rewrite rules automatically, implemented in Rust on the egg library… | ||
| egg: Fast and Extensible Equality Saturation | POPL 2021 | 2021-01-17 |
Equality saturation is implemented as the egg Rust library, which applies rewrites into an e-graph and then runs a single rebuild once per iteration rather… | ||
| nothing matches | ||