Rocq proof assistant

TensorRocq: Enabling Diagrammatic Reasoning in Rocq

Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential …

Ben Caldwell, William Spencer, Aleks Kissinger, Robert Rand