Pattern Matching in AI Compilers and its Formalization (Extended Version)

Alex Collins; Bin Fan; Joseph W. Cutler; Mahesh Ravishankar; Vinod Grover

REVIEW 3 major objections 5 minor 31 references

Pattern Matching in AI Compilers and its Formalization (Extended Version)

T0 review · 3 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that PyPM's backtracking pattern matcher is sound against a declarative semantics, mechanically checked in Coq.

desk verdict A genuinely useful account of a pattern-matching DSL for AI compilers, but the printed declarative and algorithmic semantics for existential variables don't line up, so the main equivalence theorem is unsupported as written. read the letter →

arxiv 2412.13398 v1 pith:WEOZNR6W submitted 2024-12-18 cs.PL cs.LG

Joseph W. Cutler , Alex Collins , Bin Fan , Mahesh Ravishankar , Vinod Grover This is my paper · ORCID

classification cs.PLcs.LG

keywords PyPMCorepatternmatchingrewriterulesAIcompilerscomputationgraphsCoqformalizationbacktracking

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

PyPM is a Python-embedded language for writing rewrite passes that replace pieces of machine-learning computation graphs with optimized GPU kernels; its matcher is thousands of lines of C++ and, before this work, had no specification. This paper tries to give PyPM a mathematical core. It distills the pattern language into a calculus, CorePyPM, with a declarative semantics that says which terms match which patterns and an algorithmic semantics that models the backtracking interpreter. The central result is that the two agree in the sound direction: if the machine succeeds with substitution $\theta$, the declarative relation $p \mathrel{@\theta}\approx t$ holds, and if it fails, no such substitution exists. The proof is fully mechanized in Coq, so if it is right, PyPM rests on a mechanically checkable foundation rather than on the behavior of an undocumented implementation.

What carries the argument

The load-bearing object is the matching judgment $p \mathrel{@\langle\theta,\phi\rangle}\approx t$, read 'term $t$ matches pattern $p$ with term substitution $\theta$ and function substitution $\phi$.' The argument is carried by the algorithmic state $running(\theta,\phi,stk,k)$, where $k$ is a continuation of actions such as $match(p,t)$, $guard(g)$, $checkName(x)$, and $matchConstr(p,x)$, and $stk$ is a stack of saved states. Each step either binds a variable, checks a guard, unfolds a pattern, or commits to an alternate, and conflicts backtrack by popping the stack. This machinery is what ties the executable matcher to the declarative specification: a successful run accumulates a substitution the declarative rules accept, and a failed run is one that exhausts every alternative.

What would settle it

Take pattern $\exists x.y$ and term $f(c)$, with $y$ bound to $f(c)$. Declaratively, P-Exists derives $\exists x.y \mathrel{@\{y\mapsto f(c)\}}\approx f(c)$, because the body $y$ matches and $x$ can invent any subterm. Algorithmically, starting from $running(\emptyset,[],[match(\exists x.y, f(c))])$ binds $y$, then hits $checkName(x)$ with no binding for $x$ and must backtrack to failure. So the failure half of Theorem 2 fails as stated for the full calculus unless P-Exists is restricted or checkName is changed.

Watch

Extended reading notes

Core claim

CorePyPM treats computation graphs as terms $f(t_1,\dots,t_n)$ over an operator signature, and patterns as variables, operator applications, alternates, guards, existential variables, match constraints, function variables, and recursive fixpoints. The paper defines matching twice. The declarative semantics is an inductive judgment $p \mathrel{@\langle\theta,\phi\rangle}\approx t$ in which a substitution pair witnesses the match, alternates are chosen by either rule, and existential variables invent a subterm. The algorithmic semantics is a small-step state machine $running(\theta,\phi,stk,k)$ with a continuation of directives and a backtracking stack for alternates, echoing the behavior of the C++ matcher. Theorem 2 states that the machine is sound: if $running(\varnothing,[],[match(p,t)])$ reaches $success(\theta)$, then $p \mathrel{@\theta}\approx t$ is derivable, and if it reaches $failure$, no $\theta$ makes that judgment derivable. The paper notes that the machine is not complete, since alternates are tried in order and backtracking is left-eager; soundness is the property it proves and mechanizes as $succ\_sound$ and $fail\_sound$ in Coq.

Load-bearing premise

The declarative rule for existential variables lets $\exists x.p$ match even when $x$ never appears in $p$, while the algorithm places a $checkName(x)$ obligation after matching the body, so the failure-soundness half of Theorem 2 is not established for such patterns unless the paper states a restriction that reconciles the two rules.

Editorial extensions

If this is right

If Theorem 2 holds for CorePyPM, PyPM's rewriting pass has a specification: every optimization that fires corresponds to a declarative match, so a rule can only replace subgraphs the pattern was intended to select.
Because failure is claimed to imply absence of any match, a negative answer from the matcher carries a guarantee, which matters for instruction selection: the compiler can conclude that a fused kernel does not apply to a given subgraph.
The formal calculus separates the meaning of patterns from the search order, so PyPM's alternation and backtracking behavior can be studied independently of the C++ implementation and reimplemented elsewhere.
The same declarative/algorithmic pair could be adapted to other rewrite-based AI compiler backends, giving their pattern languages specifications of comparable precision to CorePyPM's.
The evaluation shows that two hand-written PyPM rules, one for fused multi-head attention and one for GEMM epilog fusion, produce speedups across standard transformer and computer-vision inference benchmarks, evidence that the formalized features are sufficient for practical optimization patterns.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The formal core abstracts computation graphs as syntax trees, while PyPM matches graphs with shared subgraphs; making the calculus DAG-aware would require deciding whether two occurrences of a variable denote pointer-identical nodes or structurally equal terms.
Because alternates are committed to in file order, reordering pattern definitions changes which substitution a match produces; PyPM's behavior is order-sensitive even though the declarative semantics is not.
One testable extension is to run the existing C++ matcher on the CorePyPM constructs and compare each outcome to the algorithmic semantics; since the Coq proof covers the calculus rather than the C++ code, any discrepancy would isolate where the implementation must be aligned.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

You should read this paper if you care about pattern languages for rewrite systems. The authors built PyPM, a Python-embedded DSL for matching subgraphs of ML computation graphs, and they extract a core calculus (CorePyPM) with a declarative semantics plus an algorithmic backtracking semantics. The novel combination is real: recursive patterns, nondeterministic alternates, function variables (second-order), guards, and match constraints, together with a claimed Coq proof (succ_sound and fail_sound) that the algorithm is sound and complete with respect to the declarative relation. That's a meaningful step beyond prior mechanized pattern matching work like De Santo et al. on JS regexes.

The writing is honest. They explicitly say the benchmarks are not meant to show state-of-the-art speedups, only expressiveness; the related work discussion is fair, including the key comparison to Moura and Bjørner's E-matching VM. The formalization is self-contained and not fitted to any benchmark. For a paper from industry, the level of candor is refreshing.

The soft spot is not fatal to the whole enterprise, but it undermines the central theorem as printed. The declarative rule P-Exists (Fig. 16) lets you derive ∃x.p @ θ ≈ t whenever p matches with θ extended by any binding for x. There is no side condition that x actually occur in p. The algorithmic rule ST-Match-Exists (Fig. 17) runs match(p,t) followed by checkName(x), and checkName is only defined when θ(x) is bound. Take pattern ∃x.y, term c, and θ={y↦c}. The declarative judgment ∃x.y @ θ ≈ c is derivable (pick any t' for x). The algorithm binds y to c and then hits checkName(x) with x unbound. No transition applies, so the run is stuck. If you treat stuck as failure, the algorithm returns failure while a declarative witness exists, directly contradicting the failure-soundness half of Theorem 2. The same issue arises when x appears only in a guard, because the guard can't be evaluated with x unbound. The paper never states a well-formedness restriction like x ∈ FV(p). So the claimed equivalence is not established by the printed rules. The Coq proof might use different definitions, but Proof.v isn't included in the arXiv version, so I can't verify.

This is a fixable flaw: add the occurrence condition to P-Exists (and probably to the corresponding algorithmic rule), and restate the theorem under that condition. But it needs to be stated clearly, and the artifacts need to be available. A serious referee should ask for that.

I'd bring this to a reading group as an example of a well-motivated formalization effort with a concrete, teachable gap between declarative and algorithmic semantics.

Recommendation: engage with it for peer review, but require the fix and the Coq files.

Referee Report

3 major / 5 minor

Summary. The paper presents PyPM, a Python-embedded DSL for writing rewrite-based optimization passes over machine learning computation graphs, and CorePyPM, a formal core calculus intended to capture the essence of PyPM pattern matching. The formal part defines a highly nondeterministic declarative matching semantics, a backtracking algorithmic semantics with a continuation and stack, and states Theorem 2, an algorithmic-soundness result claiming that successful runs produce declarative matches and failed runs imply no match exists; the proof is said to be mechanized in Coq. The paper also describes the PyPM frontend and C++ backend, reports benchmark speedups on HuggingFace and TorchVision models for fused attention and epilog patterns, and sketches a directed-graph-partitioning use case.

Significance. If the formal claims are correct, the paper makes a useful contribution: it provides a clear declarative specification for a practical, feature-rich pattern language, an idealized algorithmic semantics, and a mechanized soundness proof, which is rare for AI-compiler infrastructure. The separation of declarative and algorithmic semantics is pedagogically valuable, and the benchmark evaluation is honest in scope: it uses external models and does not tune formalism constants to fit the data. The machine-checked proofs (succ_sound and fail_sound) are a substantial strength. However, the printed formal rules must be internally consistent with the stated theorem; the existential-variable rules, as printed, do not support the claimed failure-soundness property.

major comments (3)

[Figure 16 (P-Exists) and Figure 17 (ST-Match-Exists, ST-CheckName)] The declarative rule P-Exists has no side condition requiring the bound variable x to occur in the body pattern p, whereas the algorithmic rule ST-Match-Exists always appends checkName(x), and ST-CheckName is defined only when θ(x) is already bound. Concretely, with p = y and t = c, the judgment ∃x.y @ {y↦c} is derivable in the declarative semantics (choose any t' in P-Exists, then apply P-Var), but the algorithm binds y and then reaches checkName(x) with x unbound; none of the printed transition rules applies, so the run is stuck rather than successful or failed. If an unstated convention treats an unbound checkName as failure, the failure-soundness half of Theorem 2 is immediately false, because the declarative witness {y↦c} exists for ∃x.y against c. The same problem arises for guards, e.g., ∃x.(y ; guard(x.rank == 2)), where the declarative rule can choose t' to make the guard true but the algorithm cannot evaluate the guard without a binding for x. The paper must either restrict P-Exists to binders that occur in the body (e.g., require x ∈ FV(p)), state that restriction explicitly, and show the algorithmic semantics respects it, or change the algorithmic treatment of existential variables so that vacuous binders are handled in a way consistent with the declarative rule. As printed, Theorem 2 is not supported.
[Appendix A, Figure 18 (ST-Match-Fun-Var-Bound)] The algorithmic rule for the case where a function variable F is already bound is not well-formed: it refers to an undefined continuation k', and uses φ(x) on the left where the surrounding rules use φ(F) for function-variable lookups. The bound case should presumably continue with the argument-matching obligations k' = [match(p1,t1), ..., match(pn,tn)] as in ST-Match-Fun-Var-Bind. As printed, this part of the full-calculus algorithmic semantics cannot be checked, which matters because Theorem 2 is claimed for the full CorePyPM calculus including function variables. The authors should correct the rule and confirm it matches the Coq development.
[Appendix A, Figure 17 (ST-Match-Exists)] The target state of ST-Match-Exists is written as running(θ,stk, match(p,t)::k'), omitting the function substitution φ that is part of the running state in all other rules (including ST-Success and ST-Match-Fun). If this is a typographical omission, it should be fixed; if the rule is intended to drop φ, the rest of the semantics and the statement of Theorem 2 would need revision. Since the paper claims a mechanized proof, the printed rules should match the Coq formalization exactly.

minor comments (5)

[Section 3.1] The prose says the algorithmic semantics describes 'how to determine if a term t matches a pattern p', which suggests a decision procedure, but Section 3.5 acknowledges that recursive patterns such as μP(x).P(x) can diverge. The text should explicitly distinguish partial correctness from termination, since Theorem 2 is only a conditional soundness statement about runs that reach success or failure.
[Section 3.1, Theorem 1] Match Weakening is stated without a proof or a pointer to the Coq file in the main text; a brief proof sketch or an explicit reference to the corresponding lemma in Proof.v would help the reader verify the claim independently of the artifact.
[Section 4.2] The directed graph partitioning use case is described only as a concept and is not implemented or evaluated in the paper; it might be more appropriate to label this section as future work rather than presenting it as a demonstrated contribution.
[Throughout] The manuscript contains numerous typographical and grammatical errors (e.g., 'Univeristy', 'langauge', 'nondeterminstic', 'afformented', 'shalowly', 'distinguised', 'msut', 'replacments'), and a careful proofreading pass is needed before publication.
[Section 3.2 / Appendix A] The guard semantics uses Jg[θ]K with the substitution θ, but for guards mentioning variables not bound by the pattern, Jg[θ]K is not defined; the paper should state a well-formedness condition for guarded patterns (all variables in g must be in the domain of θ) or define a default value for unbound variables.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the Coq-verified equivalence is self-contained; the existential-variable rule mismatch is a correctness gap, not a circular reduction.

full rationale

The paper's main formal claim, Theorem 2, relates two independently specified relations: the declarative matching judgment p @ <theta, phi> approx t (Figure 16) and the backtracking state-transition interpreter (Figures 17-18). Neither relation is defined in terms of the other, and the soundness and failure-soundness proofs are mechanized in Coq (succ_sound, fail_sound), which is independent machine-checked evidence. No parameter is fitted to benchmarks; the HuggingFace and TorchVision evaluations are used only to show that hand-written PyPM patterns are expressive, not to calibrate the semantics. The only author-overlapping citation, [18] (Phothilimthana et al., including Grover), is background on swizzle patterns and is not load-bearing. The paper's own stated limitation that hand-crafted replacements must be available is an engineering limitation, not a circular step. A genuine technical caveat exists: P-Exists (Figure 16) has no side condition requiring the existential variable to occur in the body, while ST-Match-Exists (Figure 17) enforces checkName(x), so failure-soundness for vacuous existentials is unsupported by the printed rules; this is a specification gap or potential unsoundness, but it is not an instance of a prediction being equivalent to its inputs by construction. Accordingly, no circular step can be exhibited, and the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No parameters are fitted to data; the calculus is parameterized by an operator set and attribute interpretation, which are domain inputs. The main axioms are domain assumptions about the relationship between the formal model and the real PyPM system, plus a necessary but unstated restriction on existential variables. No new physical entities are introduced.

assumptions (5)

domain assumption The declarative semantics is the authoritative specification of PyPM pattern matching.
The paper defines CorePyPM as the mathematical core; it assumes this formal spec captures the intended behavior of the PyPM language (Section 3).
domain assumption The algorithmic semantics is an accurate idealization of the actual C++ matcher in DLCB.
Section 2.4 describes the C++ implementation; Section 3 presents the algorithmic semantics as 'a stylized account' and does not prove the implementation matches it.
ad hoc to paper Existential pattern variables are always bound by the body pattern; the declarative rule P-Exists (Figure 9) is read with this restriction.
The algorithmic semantics ST-Match-Exists (Figure 17) uses checkName(x) to require a binding, but the printed declarative rule does not state this requirement; this mismatch is unexplained and affects the soundness theorem.
domain assumption Attribute guards (x.shape.rank etc.) are faithfully represented by the abstract attribute interpretation J·K.
Section 3.2 abstracts tensor attributes to a fixed set A with interpretation J·K; the paper assumes this abstraction matches actual Tensor attributes.
standard math The Coq proof assistant is sound.
The mechanized proof relies on the soundness of Coq's logic (Section 3, Theorem 2 proof).

how reviews work

0 comments

Cite this review

Pith. "Pith review of Pattern Matching in AI Compilers and its Formalization (Extended Version)." pith.science (2026). https://pith.science/paper/WEOZNR6W

@misc{pith2026241213398,
  author       = {Pith},
  title        = {Pith review of: Pattern Matching in AI Compilers and its Formalization (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WEOZNR6W}},
  note         = {Machine review of arXiv:2412.13398}
}

read the original abstract

PyPM is a Python-based domain specific language (DSL) for building rewrite-based optimization passes on machine learning computation graphs. Users define individual optimizations by writing (a) patterns that match subgraphs of a computation graph and (b) corresponding rules which replace a matched subgraph with an optimized kernel. PyPM is distinguished from the many other DSLs for defining rewriting passes by its complex and novel pattern language which borrows concepts from logic programming. PyPM patterns can be recursive, nondeterminstic, and can require checking domain-specific constraints such as the shapes of tensors. The PyPM implementation is thus similarly complicated, consisting of thousands of lines of C++ code. In this paper, we present our work on building PyPM, as well as formalizing and distilling and this complexity to an understandable mathematical core. We have developed a formal core calculus expressing the main operations of the PyPM pattern language. We define both a declarative semantics - describing which patterns match which terms - and an algorithmic semantics - an idealized version of the PyPM pattern interpreter - and prove their equivalence. The development is fully mechanized in the Coq proof assistant.

Figures

Figures reproduced from arXiv: 2412.13398 by the authors.

**Figure 1.** cuBLAS Pattern Example Trans(y). Because patterns can be large and often include a great deal of sharing, programmers can bind sub-patterns to local names. These local variable names do not get their own bindings in the substitution, they are merely aliases. The pattern definition MMxyT also demonstrates another feature of PyPM, namely constraints. This pattern does not match merely any subgraph that looks like 𝑥𝑦𝑇 … view at source ↗

**Figure 2.** Alternate GELU Pattern @pattern def UnaryChain(x,f): return f(UnaryChain(x,f)) @pattern def UnaryChain(x,f): return f(x) [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 5.** Grammar of Terms and Basic Patterns setup can be thought of through the analogy of PyPM with logic languages. The declarative semantics can be thought of as a proof system for pattern matching: given a witness, verify that the formula is satisfied. Meanwhile, the algorithmic semantics defines a proof search procedure for the logic: search for a witness to the formula. In Section 3.1, we describe the minimal subset … view at source ↗

Figures from the paper (11 more)

**Figure 6.** Figure 6: Declarative Semantics of Basic Patterns of pattern alternates (and other features we’ll see later), not all ground patterns are terms, and so we must specify what it means to “match” with an inductive relation. Theorem 1 (Match Weakening). If 𝑝 @𝜃 ≈ 𝑡 and 𝜃 ⊆ 𝜃 ′ then …

**Figure 7.** Figure 7: Algorithmic Semantics of Basic Patterns 𝑒 ::= 𝑡 .𝛼 | 𝑥.𝛼 | 𝑒 + 𝑒 | 𝑒 − 𝑒 | . . . 𝑔 ::= 𝑒 = 𝑒 ′ | 𝑒 < 𝑒 ′ | 𝑔 ∧ 𝑔 ′ | 𝑔 ∨ 𝑔 ′ | ¬𝑔 𝑝 ::= · · · | 𝑝 ; guard (𝑔) P-Guard 𝑝 @𝜃 ≈ 𝑡 J𝑔[𝜃]K = True 𝑝 ; guard (𝑔) @𝜃 ≈ 𝑡 [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]

**Figure 8.** Figure 8: Guarded Pattern Syntax and Declarative Semantics Guards, written 𝑔, are boolean constraints over arithmetic expressions. Those arithmetic expressions can include terms like 𝑥.𝛼, where 𝑥 is a pattern variable, and 𝛼 is an attribute. While PyPM defines a concrete set of …

**Figure 9.** Figure 9: Syntax and Declarative Semantics of Existential Variables and Match Constraints such that 𝑝 matches against𝑡 under 𝜃∪{𝑥 ↦→ 𝑡 ′ }. Meanwhile, 𝑝 ; (𝑝 ′ ≈ 𝑥) matches against 𝑡 under 𝜃 if 𝑝 matches against 𝑡, and 𝜃 (𝑥) matches against 𝑝 ′ . These two constructs highlight …

**Figure 10.** Figure 10: HuggingFace Benchmarks side — there are simply too many options. A natural idea in this scenario is to create the right hand side rule “just in time”. When we find a match, we can pass the subgraph off to an AI compiler that can build the fused kernel, and use the res…

**Figure 14.** Figure 14: Matrix Multiplication Epilog Patterns the computation. These are opposing solutions to similar problems — one manual, the other automatic. However, one could in principle use DLCB in concert with a scheduling language to further optimize the scheduled code. The idea o…

**Figure 13.** Figure 13: TorchVision Compile Time Cost is laid out. The point of a scheduling langauge is to let the programmer manually specify the way that a computation is executed on a device. Meanwhile, DLCB exists to take naively-generated model code (i.e. without a schedule), and use r…

**Figure 15.** Figure 15: Grammar of Terms and Patterns P-Var 𝜃 (𝑥) ↦→ 𝑡 𝑥 @ ⟨𝜃, 𝜙⟩ ≈ 𝑡 P-Fun ∀𝑖. (𝑝𝑖 @ ⟨𝜃, 𝜙⟩ ≈ 𝑡𝑖) 𝑓 (𝑝1, . . . , 𝑝𝑛) @ ⟨𝜃, 𝜙⟩ ≈ 𝑓 (𝑡1, . . . , 𝑡𝑛) P-Alt-1 𝑝 @ ⟨𝜃, 𝜙⟩ ≈ 𝑡 𝑝∥𝑝 ′ @ ⟨𝜃, 𝜙⟩ ≈ 𝑡 P-Alt-2 𝑝 ′ @ ⟨𝜃, 𝜙⟩ ≈ 𝑡 𝑝∥𝑝 ′ @ ⟨𝜃, 𝜙⟩ ≈ 𝑡 P-Guard 𝑝 @ ⟨𝜃, 𝜙⟩ ≈ 𝑡 J𝑔[𝜃]K = True 𝑝 ; g…

**Figure 16.** Figure 16: Declarative Semantics [PITH_FULL_IMAGE:figures/full_fig_p016_16.png]

**Figure 17.** Figure 17: Algorithmic Semantics Part 1 [PITH_FULL_IMAGE:figures/full_fig_p017_17.png]

**Figure 18.** Figure 18: Algorithmic Semantics Part 2 [PITH_FULL_IMAGE:figures/full_fig_p018_18.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 13 canonical work pages

[1]

Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dandelion Mané, Rajat Monga, Sherry Moore, Derek Murra...

2015
[2]

L Susan Blackford, Antoine Petitet, Roldan Pozo, Karin Remington, R Clint Whaley, James Demmel, Jack Dongarra, Iain Duff, Sven Ham- marling, Greg Henry, et al. 2002. An updated set of basic linear algebra subprograms (BLAS). ACM Trans. Math. Software28, 2 (2002), 135–151

2002
[3]

Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Meghan Cowan, Haichen Shen, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: an automated end-to-end optimizing compiler for deep learning. In Pro- ceedings of the 13th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, ...

work page 2018
[4]

Tri Dao, Dan Fu, Stefano Ermon, Atri Rudra, and Christopher Ré
[5]

Noé De Santo, Aurèle Barrière, and Clément Pit-Claudel. 2024. A Coq Mechanization of JavaScript Regular Expression Semantics. Proc. ACM Program. Lang. 8, ICFP, Article 270 (aug 2024), 29 pages. https: //doi.org/10.1145/3674666

doi:10.1145/3674666 2024
[6]

The Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project. http://coq.inria.fr Version 8.0

work page 2004
[7]

Satoshi Egi and Yuichi Nishiwaki. 2020. Functional Programming in Pattern-Match-Oriented Programming Style. arXiv preprint arXiv:2002.06176 (2020)

work page arXiv 2020
[8]

Roy Frostig, Matthew Johnson, and Chris Leary. 2018. Compiling machine learning programs via high-level tracing. https://mlsys.org/ Conferences/doc/2018/146.pdf

work page 2018

Show all 31 references

[9]

Bastian Hagedorn, Johannes Lenfers, Thomas Kundefinedhler, Xuey- ing Qin, Sergei Gorlatch, and Michel Steuwer. 2020. Achieving high- performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies. Proc. ACM Program. Lang. ...

2020 doi
[10]

Dan Hendrycks and Kevin Gimpel. 2016. Gaussian error linear units (gelus). arXiv preprint arXiv:1606.08415 (2016)

2016 arXiv
[11]

Yuka Ikarashi, Gilbert Louis Bernstein, Alex Reinking, Hasan Genc, and Jonathan Ragan-Kelley. 2022. Exocompilation for productive programming of hardware accelerators. InProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementat...

2022
[12]

Robert Kowalski. 2014. Logic Programming. In Computational Logic, Jörg H. Siekmann (Ed.). Handbook of the History of Logic, Vol. 9. North-Holland, 523–569. https://doi.org/10.1016/B978-0-444-51624- 4.50012-5

2014 doi
[13]

Robert Kowalski and Steve Smoliar. 1982. Logic for problem solving. SIGSOFT Softw. Eng. Notes 7, 2 (apr 1982), 61–62. https://doi.org/10. 1145/1005937.1005947

1982
[14]

Miller and G

D. Miller and G. Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press. https://books.google.com/books? id=xKsgAwAAQBAJ

2012
[15]

Leonardo Moura and Nikolaj Bjørner. 2007. Efficient E-Matching for SMT Solvers. In Proceedings of the 21st International Conference on Automated Deduction: Automated Deduction (Bremen, Germany) (CADE-21). Springer-Verlag, Berlin, Heidelberg, 183–198. https://doi. org/10.1007/9...

2007 doi
[16]

Nvidia. [n. d.]. cuBLAS Documentation. https://docs.nvidia.com/cuda/ cublas/. Accessed: 2014-09-10

2014
[17]

Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Brad- bury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Yang, Zach DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu F...

2019
[18]

Kaufman, Vinod Grover, Emina Torlak, and Rastislav Bodik

Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, and Rastislav Bodik. 2019. Swizzle Inventor: Data Movement Synthesis for GPU Kernels. In Pro- ceedings of the T...

2019
[19]

Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, and Saman Amarasinghe. 2013. Halide: a lan- guage and compiler for optimizing parallelism, locality, and recom- putation in image processing pipelines. In Proceedings of the 34th ACM SIGPLAN Con...

2013
[20]

Amit Sabne. 2020. XLA : Compiling Machine Learning for Peak Per- formance

2020
[21]

Michel Steuwer, Toomas Remmelg, and Christophe Dubach. 2016. Matrix multiplication beyond auto-tuning: Rewrite-based GPU code generation. In 2016 International Conference on Compliers, Architectures, and Sythesis of Embedded Systems (CASES) . 1–10. https://doi.org/10. CGO ’25,...

2016
[22]

Jonathan Van der Cruysse and Christophe Dubach. 2024. Latent Id- iom Recognition for a Minimalist Functional Array Language Us- ing Equality Saturation. In Proceedings of the 2024 IEEE/ACM In- ternational Symposium on Code Generation and Optimization (Ed- inburgh, United Kingd...

2024
[23]

Lee, James Bornholt, and Adrian Sampson

Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. 2021. Vectorization for digital signal proces- sors via equality saturation. In Proceedings of the 26th ACM Inter- national Conference on Architectural Support for Programming Lan- guages and Op...

2021
[24]

Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N

Ashish Vaswani, Noam M. Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. 2017. Attention is All you Need. In Neural Information Processing Systems . https://api.semanticscholar.org/CorpusID:13756489

2017
[25]

Jan Wielemaker, Tom Schrijvers, Markus Triska, and Torbjörn Lager
[26]

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and exten- sible equality saturation. Proc. ACM Program. Lang. 5, POPL, Article 23 (jan 2021), 29 pages. https://doi.org/10.1145/3434304

2021 doi
[27]

Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Rémi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gugger, Mari...

2019 arXiv
[28]

Yichen Yang, Phitchaya Phothilimthana, Yisu Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. 2021. Equality saturation for tensor graph superoptimization. Proceedings of Machine Learning and Systems 3 (2021), 255–268

2021
[29]

Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation. Proc. ACM Program. Lang. 7, PLDI, Article 125 (jun 2023), 25 pages. https://doi.org/10.1145/3...

2023 doi
[2012]

Theory and Practice of Logic Programming 12, 1-2 (2012), 67–96

SWI-Prolog. Theory and Practice of Logic Programming 12, 1-2 (2012), 67–96

2012
[2022]

Advances in Neural Information Processing Systems 35 (2022), 16344–16359

Flashattention: Fast and memory-efficient exact attention with io-awareness. Advances in Neural Information Processing Systems 35 (2022), 16344–16359

2022

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [1]

Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dandelion Mané, Rajat Monga, Sherry Moore, Derek Murra...

2015

[2] [2]

L Susan Blackford, Antoine Petitet, Roldan Pozo, Karin Remington, R Clint Whaley, James Demmel, Jack Dongarra, Iain Duff, Sven Ham- marling, Greg Henry, et al. 2002. An updated set of basic linear algebra subprograms (BLAS). ACM Trans. Math. Software28, 2 (2002), 135–151

2002

[3] [3]

Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Meghan Cowan, Haichen Shen, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: an automated end-to-end optimizing compiler for deep learning. In Pro- ceedings of the 13th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, ...

work page 2018

[4] [4]

Tri Dao, Dan Fu, Stefano Ermon, Atri Rudra, and Christopher Ré

[5] [5]

Noé De Santo, Aurèle Barrière, and Clément Pit-Claudel. 2024. A Coq Mechanization of JavaScript Regular Expression Semantics. Proc. ACM Program. Lang. 8, ICFP, Article 270 (aug 2024), 29 pages. https: //doi.org/10.1145/3674666

doi:10.1145/3674666 2024

[6] [6]

The Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project. http://coq.inria.fr Version 8.0

work page 2004

[7] [7]

Satoshi Egi and Yuichi Nishiwaki. 2020. Functional Programming in Pattern-Match-Oriented Programming Style. arXiv preprint arXiv:2002.06176 (2020)

work page arXiv 2020

[8] [8]

Roy Frostig, Matthew Johnson, and Chris Leary. 2018. Compiling machine learning programs via high-level tracing. https://mlsys.org/ Conferences/doc/2018/146.pdf

work page 2018