Cover Image

Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Zucker, Philip
Format:	Preprint
Published:	2025
Subjects:	Programming Languages F.4.1
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Stratified Type Theory
by: Chan, Jonathan, et al.
Published: (2023)

Verifying Tree-Manipulating Programs via CHCs
by: Faella, Marco, et al.
Published: (2025)

A Graphical Interface for Category Theory Proofs in Coq
by: Chabassier, Luc
Published: (2025)

Reimplementing Mizar in Rust
by: Carneiro, Mario
Published: (2023)

Lean4Lean: Verifying a Typechecker for Lean, in Lean
by: Carneiro, Mario
Published: (2024)

Two-Level Type Theory and Applications
by: Annenkov, Danil, et al.
Published: (2017)

Intersection Types for a Computational Lambda-Calculus with Global State
by: de'Liguoro, Ugo, et al.
Published: (2021)

Abstract clones for abstract syntax
by: Arkor, Nathanael, et al.
Published: (2021)

Ground Stratification for a Logic of Definitions with Induction
by: Guermond, Nathan, et al.
Published: (2025)

LeanLTL: A unifying framework for linear temporal logics in Lean
by: Vin, Eric, et al.
Published: (2025)

Extending the Quantitative Pattern-Matching Paradigm
by: Alves, Sandra, et al.
Published: (2024)

SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
by: Hansen, Zachary, et al.
Published: (2025)

Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions
by: Bhusal, Bishnu, et al.
Published: (2025)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
by: Xu, Qiyuan, et al.
Published: (2024)

The Lambda Calculus is Quantifiable
by: Maestracci, Valentin, et al.
Published: (2024)

AdapTT: Functoriality for Dependent Type Casts
by: Adjedj, Arthur, et al.
Published: (2025)

Genericity Through Stratification
by: Arrial, Victor, et al.
Published: (2024)

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
by: Bobrow, Elliot, et al.
Published: (2025)

Bottom-up computation using trees of sublists (Functional Pearl)
by: Mu, Shin-Cheng
Published: (2023)

Definitional Functoriality for Dependent (Sub)Types -- Extended version
by: Laurent, Théo, et al.
Published: (2023)

Introducing Divergence for Infinite Probabilistic Models
by: Finkel, Alain, et al.
Published: (2023)

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi
by: Cerda, Rémy
Published: (2025)

What does it take to certify a conversion checker?
by: Lennon-Bertrand, Meven
Published: (2025)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
by: Bertrand, Meven Lennon, et al.
Published: (2026)

Cartesian Differential Kleisli Categories
by: Lemay, Jean-Simon Pacaud
Published: (2023)

The Cost of Skeletal Call-by-Need, Smoothly
by: Accattoli, Beniamino, et al.
Published: (2025)

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
by: Sundaram, Aarthi, et al.
Published: (2021)

Gödel Mirror: A Formal System For Contradiction-Driven Recursion
by: Chan, Jhet
Published: (2025)

Orbit-finite linear programming
by: Ghosh, Arka, et al.
Published: (2023)

A Nivat Theorem for Weighted Alternating Automata over Commutative Semirings
by: Grabolle, Gustav
Published: (2022)

A Theory of Hanoi Omega-Automata and Games
by: Filiot, Emmanuel, et al.
Published: (2026)

GeoGalactica: A Scientific Large Language Model in Geoscience
by: Lin, Zhouhan, et al.
Published: (2023)

Random Variables, Conditional Independence and Categories of Abstract Sample Spaces
by: Stein, Dario
Published: (2025)

Type Theory with Single Substitutions
by: Kaposi, Ambrus, et al.
Published: (2025)

Sensible Intersection Type Theories
by: Dezani-Ciancaglini, Mariangiola, et al.
Published: (2026)

The Latent Space of Equational Theories
by: Berlioz, Luis, et al.
Published: (2026)

Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
by: Lahiri, Shuvendu K.
Published: (2024)

Characterizing NC1 with Typed Monoids
by: Dawar, Anuj, et al.
Published: (2025)

Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
by: Koomullil, George
Published: (2026)

The Relational Machine Calculus
by: Barrett, Chris, et al.
Published: (2024)