Cover Image

TensorRocq: Enabling diagrammatic reasoning in Rocq

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Caldwell, Benjamin, Spencer, William, Kissinger, Aleks, Rand, Robert
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

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

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

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

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

Adhesive category theory for graph rewriting in Rocq
by: Arsac, Samuel, et al.
Published: (2025)

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

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

Multi types and reasonable space
by: Accattoli, Beniamino, et al.
Published: (2022)

Complete first-order reasoning for functional programs
by: Murali, Adithya, et al.
Published: (2026)

Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
by: Voichick, Finn, et al.
Published: (2022)

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

Automatic Goal Clone Detection in Rocq
by: Ghanbari, Ali
Published: (2025)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
by: Ye, Kangfeng, et al.
Published: (2023)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

On the Expressivity of Typed Concurrent Calculi
by: Paulus, Joseph William Neal
Published: (2024)

Partial Incorrectness Logic
by: Verscht, Lena, et al.
Published: (2025)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
by: Li, Runming, et al.
Published: (2025)

Formal P-Category Theory and Normalization by Evaluation in Rocq
by: Berry, David G., et al.
Published: (2025)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
by: Batz, Kevin, et al.
Published: (2024)

Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi
by: Gao, Dichuan, et al.
Published: (2026)

Finite-Choice Logic Programming
by: Martens, Chris, et al.
Published: (2024)

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)

A complete logic for causal consistency
by: Simmons, Will, et al.
Published: (2024)

Weighted GKAT: Completeness and Complexity
by: Van Koevering, Spencer, et al.
Published: (2025)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
by: Rao, Balaji, et al.
Published: (2026)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
by: Yubeaton, Patrick, et al.
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
by: Zhang, Cheng, et al.
Published: (2026)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)

Can LLMs Perform Synthesis?
by: Egolf, Derek, et al.
Published: (2026)

Type Theory With Erasure
by: Theocharis, Constantine, et al.
Published: (2026)

A Program Logic for Abstract (Hyper)Properties
by: Baldan, Paolo, et al.
Published: (2026)

Ordered Adjoint Logic (Extended Version)
by: Roshal, Sophia, et al.
Published: (2026)

Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
by: Bembenek, Aaron, et al.
Published: (2026)