Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Algebraic coherent confluence and higher globular Kleene algebras
(Submitted on 29 Jun 2020 (v1), last revised 24 Nov 2022 (this version, v5))
Abstract: 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-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.
Submission history
From: Philippe Malbos [view email] [via LOGICAL proxy][v1] Mon, 29 Jun 2020 15:47:06 GMT (40kb)
[v2] Wed, 26 Aug 2020 14:08:52 GMT (41kb)
[v3] Thu, 7 Apr 2022 17:38:54 GMT (48kb)
[v4] Tue, 19 Jul 2022 14:18:16 GMT (55kb)
[v5] Thu, 24 Nov 2022 14:53:24 GMT (107kb,D)
Link back to: arXiv, form interface, contact.