Copertina

Adhesive category theory for graph rewriting in Rocq

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Arsac, Samuel, Harmer, Russ, Pous, Damien
Natura:	Preprint
Pubblicazione:	2025
Soggetti:	Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

String Diagrams for Monoidal Categories, in Rocq
di: Pous, Damien
Pubblicazione: (2026)

A finite presentation of graphs of treewidth at most three
di: Doumane, Amina, et al.
Pubblicazione: (2024)

Continuous Algebras with Hypotheses
di: Mulder, Lukas, et al.
Pubblicazione: (2026)

On Tools for Completeness of Kleene Algebra with Hypotheses
di: Pous, Damien, et al.
Pubblicazione: (2022)

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
di: Rosain, Johann, et al.
Pubblicazione: (2026)

TensorRocq: Enabling diagrammatic reasoning in Rocq
di: Caldwell, Benjamin, et al.
Pubblicazione: (2026)

Revisiting the Fast Fourier Transform in Rocq
di: Théry, Laurent
Pubblicazione: (2022)

A Rocq Formalization of Monomial and Graded Orders
di: Boldo, Sylvie, et al.
Pubblicazione: (2025)

A Rocq Formalization of Simplicial Lagrange Finite Elements
di: Boldo, Sylvie, et al.
Pubblicazione: (2026)

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
di: Baudart, Guillaume, et al.
Pubblicazione: (2026)

Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
di: Biernacka, Małgorzata, et al.
Pubblicazione: (2022)

Nominal Sets in Rocq
di: Paranhos, Fabrício Sanches, et al.
Pubblicazione: (2025)

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
di: Kozyrev, Andrei, et al.
Pubblicazione: (2025)

Hypergraph rewriting and Causal structure of $λ-$calculus
di: Bajaj, Utkarsh
Pubblicazione: (2024)

Globular weak $ω$-categories as models of a type theory
di: Benjamin, Thibaut, et al.
Pubblicazione: (2021)

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
di: Arias, Jaime, et al.
Pubblicazione: (2024)

The $\infty$-category of $\infty$-categories in simplicial type theory
di: Gratzer, Daniel, et al.
Pubblicazione: (2026)

Incompleteness theorems via Turing category
di: Savelyev, Yasha
Pubblicazione: (2024)

RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
di: Kozyrev, Andrei, et al.
Pubblicazione: (2026)

A type theory for invertibility in weak $ω$-categories
di: Benjamin, Thibaut, et al.
Pubblicazione: (2026)

On first-order transductions of classes of graphs
di: Braunfeld, Samuel, et al.
Pubblicazione: (2022)

Monoidal weak omega-categories as models of a type theory
di: Benjamin, Thibaut
Pubblicazione: (2021)

Left-Linear Rewriting in Adhesive Categories
di: Baldan, Paolo, et al.
Pubblicazione: (2024)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
di: Viennot, Jules, et al.
Pubblicazione: (2025)

Effect Algebras as Omega-categories
di: Perticone, Lorenzo, et al.
Pubblicazione: (2023)

Decomposition horizons and a characterization of stable hereditary classes of graphs
di: Braunfeld, Samuel, et al.
Pubblicazione: (2022)

Undecidability of theories of semirings with fixed points
di: Das, Anupam, et al.
Pubblicazione: (2025)

Bringing closure to theory combination properties
di: Toledo, Guilherme V., et al.
Pubblicazione: (2026)

Strong negation in the theory of computable functionals TCF
di: Köpp, Nils, et al.
Pubblicazione: (2022)

On proving consistency of equational theories in Bounded Arithmetic
di: Beckmann, Arnold, et al.
Pubblicazione: (2022)

Being polite is not enough (and other limits of theory combination)
di: Toledo, Guilherme V., et al.
Pubblicazione: (2025)

Decomposing graphs into stable and ordered parts
di: Buffière, Hector, et al.
Pubblicazione: (2025)

Compositional Taylor expansion in cartesian differential categories
di: Walch, Aymeric
Pubblicazione: (2025)

The category of well-filtered dcpos is not $Γ$-faithful
di: Miao, Hualin, et al.
Pubblicazione: (2024)

The proof theory and semantics of second-order (intuitionistic) tense logic
di: Becker, Justus, et al.
Pubblicazione: (2026)

Wider systems for linear logic with fixed points: proof theory and complexity
di: Das, Anupam, et al.
Pubblicazione: (2026)

A formulation of D-institution using functor categories
di: Hashimoto, Go
Pubblicazione: (2026)

Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
di: Ackerman, Nathanael L., et al.
Pubblicazione: (2023)

Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$
di: de Jong, Tom
Pubblicazione: (2024)

A proof theory of (omega-)context-free languages, via non-wellfounded proofs
di: Das, Anupam, et al.
Pubblicazione: (2024)