Algebraic coherent confluence and higher globular Kleene algebras
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Ro...
Main Authors: | Cameron Calk, Eric Goubault, Philippe Malbos, Georg Struth |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2022-11-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/6743/pdf |
Similar Items
-
Modularizing the Elimination of r=0 in Kleene Algebra
by: Christopher Hardin
Published: (2005-12-01) -
Globular: an online proof assistant for higher-dimensional rewriting
by: Krzysztof Bar, et al.
Published: (2018-01-01) -
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras
by: Brijesh Dongol, et al.
Published: (2021-02-01) -
Deciding Kleene Algebras in Coq
by: Thomas Braibant, et al.
Published: (2012-03-01) -
From Kleisli Categories to Commutative C*-algebras: Probabilistic Gelfand Duality
by: Robert W. J. Furber, et al.
Published: (2015-06-01)