3 papers
cs.LO2026
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…
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.LO2026
List types for resource aware languages: an implicit name approach
Silvia Ghilezan, Jelena IvetiÄ, Pierre Lescanne +1
A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted lan…