:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Arsac, Samuel, Harmer, Russ, Pous, Damien
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2509.17392
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

String Diagrams for Monoidal Categories, in Rocq
by: Pous, Damien
Published: (2026)

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

Continuous Algebras with Hypotheses
by: Mulder, Lukas, et al.
Published: (2026)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Incompleteness theorems via Turing category
by: Savelyev, Yasha
Published: (2024)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Compositional Taylor expansion in cartesian differential categories
by: Walch, Aymeric
Published: (2025)

Model checking strategy-controlled systems in rewriting logic
by: Rubio, Rubén, et al.
Published: (2024)

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

Hypercubical manifolds in homotopy type theory
by: Mimram, Samuel, et al.
Published: (2025)

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

Classifying covering types in homotopy type theory
by: Mimram, Samuel, et al.
Published: (2025)