167 citations · 318 across the 13 of their papers we have counts for
15 papers
Finite Functional Programming
Michael Arntzenius, Max Willsey
We unify functional and logic programming by treating predicatesas functions equipped with their support: the set of inputs whose output is nonzero. Datalog, for instance, is a lan…
Optimism in Equality Saturation
Russel Arbore, Alvin Cheung, Max Willsey
Equality saturation is a program optimization technique based on non-destructive rewriting and a form of abstract interpretation called e-class analysis. Existing e-class analyses…
Stream programs are monoid homomorphisms with state
Tyler Hou, Michael Arntzenius, Max Willsey
We define a broad class of deterministic stream functions and show they can be implemented as homomorphisms into a "state" monoid. The homomorphism laws are simpler than the condit…
Better Together: Unifying Datalog and Equality Saturation
Yihong Zhang, Yisu Remy Wang, Oliver Flatt +5
We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, it supports efficient incremental execution, cooperating analyses…
Free Join: Unifying Worst-Case Optimal and Traditional Joins
Yisu Remy Wang, Max Willsey, Dan Suciu
Over the last decade, worst-case optimal join (WCOJ) algorithms have emerged as a new paradigm for one of the most fundamental challenges in query processing: computing joins effic…
babble: Learning Better Abstractions with E-Graphs and Anti-Unification
David Cao, Rose Kunkel, Chandrakana Nandi +3
Library learning compresses a given corpus of programs by extracting common structure from the corpus into reusable library functions. Prior work on library learning suffers from t…
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey +2
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification…
Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi, Max Willsey, Amy Zhu +6
Many compilers, synthesizers, and theorem provers rely on rewrite rules to simplify expressions or prove equivalences. Developing rewrite rules can be difficult: rules may be subtl…
Co-Optimization of Design and Fabrication Plans for Carpentry
Haisen Zhao, Max Willsey, Amy Zhu +4
Past work on optimizing fabrication plans given a carpentry design can provide Pareto-optimal plans trading off between material waste, fabrication time, precision, and other consi…
Relational E-Matching
Yihong Zhang, Yisu Remy Wang, Max Willsey +1
We present a new approach to e-matching based on relational join; in particular, we apply recent database query execution techniques to guarantee worst-case optimal run time. Compa…
Co-Optimization of Design and Fabrication Plans for Carpentry: Supplemental Material
Haisen Zhao, Max Willsey, Amy Zhu +4
Past work on optimizing fabrication plans given a carpentry design can provide Pareto-optimal plans trading off between material waste, fabrication time, precision, and other consi…
Equality Saturation for Tensor Graph Superoptimization
Yichen Yang, Phitchaya Mangpo Phothilimtha, Yisu Remy Wang +3
One of the major optimizations employed in deep learning frameworks is graph rewriting. Production frameworks rely on heuristics to decide if rewrite rules should be applied and in…
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang +3
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a mor…
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson +4
Recent program synthesis techniques help users customize CAD models(e.g., for 3D printing) by decompiling low-level triangle meshes to Constructive Solid Geometry (CSG) expressions…
Design and Implementation of Concurrent C0
Max Willsey, Rokhini Prabhu, Frank Pfenning
We describe Concurrent C0, a type-safe C-like language with contracts and session-typed communication over channels. Concurrent C0 supports an operation called forwarding which all…