Cover Image

A Formalization of Abstract Rewriting in Agda

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Arkle, Sam, Polonsky, Andrew
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Logic 68Q42 (Primary) 68V15 (Secondary)
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Higher-Order Pattern Unification Modulo Similarity Relations
by: Dundua, Besik, et al.
Published: (2025)

Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)
by: Nishida, Naoki, et al.
Published: (2026)

Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)
by: Nishida, Naoki
Published: (2026)

SMB algebras II: On the Constraint Satisfaction Problem over Semilattices of Mal'cev Blocks
by: Marković, Petar, et al.
Published: (2026)

Single-set cubical categories and their formalisation with a proof assistant (extended version)
by: Malbos, Philippe, et al.
Published: (2024)

Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification (Full Version)
by: Kojima, Misaki, et al.
Published: (2026)

Hyperfiniteness on Topological Ramsey Spaces
by: Bursics, Balázs, et al.
Published: (2024)

Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
by: Nakano, Keisuke, et al.
Published: (2024)

The continuous functional calculus in Lean
by: Dedecker, Anatole, et al.
Published: (2025)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)

The Solver's Paradox in Formal Problem Spaces
by: Rosko, Milan
Published: (2025)

Choiceless Polynomial Space
by: Ferrarotti, Flavio, et al.
Published: (2024)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

Higher Catoids, Higher Quantales and their Correspondences
by: Calk, Cameron, et al.
Published: (2023)

Undefinability of Approximation of 2-to-2 Games
by: Dawar, Anuj, et al.
Published: (2025)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)

Unifying lower bounds for algebraic machines, semantically
by: Seiller, Thomas, et al.
Published: (2018)

Dependence and Independence for Reversible Process Calculi
by: Aubert, Clément, et al.
Published: (2024)

Some derivations among Logarithmic Space Bounded Counting Classes
by: Janaki, V., et al.
Published: (2023)

A Minimal Substitution Basis for the Kalmár Elementary Functions
by: Prunescu, Mihai, et al.
Published: (2025)

Descriptive Complexity of Sensitivity of Cellular Automata
by: Favereau, Tom, et al.
Published: (2025)

Sample completion, structured correlation, and Netflix problems
by: Coregliano, Leonardo N., et al.
Published: (2025)

Optimal Simultaneous Byzantine Agreement, Common Knowledge and Limited Information Exchange
by: van der Meyden, Ron
Published: (2025)

A classification of bisimilarities for general Markov decision processes
by: Moroni, Martín Santiago, et al.
Published: (2024)

The complexity of bisimilarity on pointmass processes
by: Moroni, Martín Santiago, et al.
Published: (2026)

Provability in BI's Sequent Calculus is Decidable
by: Gheorghiu, Alexander, et al.
Published: (2021)

Constraint Satisfaction Problems over Finitely Bounded Homogeneous Structures: a Dichotomy between FO and L-hard
by: Dorochko, Leonid, et al.
Published: (2026)

Internalizing Extensions in Lattices of Type Theories
by: Chan, Jonathan
Published: (2025)

Bounded First-Class Universe Levels in Dependent Type Theory
by: Chan, Jonathan, et al.
Published: (2025)

A correspondence between the time and space complexity
by: Latkin, Ivan V.
Published: (2023)

Variants of Solovay reducibility
by: Titov, Ivan
Published: (2024)

Languages of Words of Low Automatic Complexity Are Hard to Compute
by: Chen, Joey, et al.
Published: (2025)

Polygraphs: From Rewriting to Higher Categories
by: Ara, Dimitri, et al.
Published: (2023)

Practical Livelock Analysis in Parameterized Unidirectional Rings
by: Farahat, Aly
Published: (2026)

Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
by: Linhares, Alexandre
Published: (2026)

Term rewriting on nestohedra
by: Curien, Pierre-Louis, et al.
Published: (2024)

Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics
by: Jaber, Guilhem, et al.
Published: (2025)

Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers
by: Ceragioli, Lorenzo, et al.
Published: (2024)

Algebraic Proof Theory for Infinitary Action Logic
by: Fussner, Wesley, et al.
Published: (2025)