3 papers
cs.LO2026
Continuous Algebras with Hypotheses
Lukas Mulder, Damien Pous, Jana Wagemaker
In the literature on Kleene algebra (KA), a number of variants have been proposed such as Kleene algebra with tests, commutative KA, bi-KA, and concurrent KA. The equational theori…
cs.LO2026
String Diagrams for Monoidal Categories, in Rocq
Damien Pous
We present a Rocq library for monoidal categories, which includes a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if…
cs.LO2025
Adhesive category theory for graph rewriting in Rocq
Samuel Arsac, Russ Harmer, Damien Pous
We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bott…