Publications

We introduce higher globular Kleene algebras and prove coherent, formal versions of classic rewriting results.

C Calk, E Goubault, P Malbos, G Struth

arXiv:2006.16129 (2020)

Accepted by Logical Methods in Computer Science (LMCS) in July 2022.

We formalise the notion of normalisation strategy, from abstract rewriting, in the formal algebraic setting of higher Kleene algebra. This leads to a succinct algebraic proof of the Squier coherence theorem for abstract rewriting systems.

C Calk, E Goubault, P Malbos

RAMICS 2021, LNCS proceedings volume 13027 (2021)

We generalise the notion of small category as a set equipped with multi-operations, and link these to modal quantales, in particular exploring the locality axiom for the domain operator.

C Calk, U Fahrenberg, C Johansen, G Struth, K Ziemanski

RAMICS 2021, LNCS proceedings volume 13027 (2021)

By equipping natural homotopy with a composition pairing, a notion due to T Porter, we show that time-reversal is captured by categorical opposition.

C Calk, E Goubault, P Malbos

Homology, Homotopy and Applications, Volume 22 Number 2 (2020)