This paper combines the two lines of research on Kleene-algebraic and higher rewriting into a unified framework. It is shown how some calculational confluence proofs in Kleene algebras, such as the Church-Rosser theorem and Newmann’s lemma, are to be extended to coherent confluence proofs. To this end, the authors introduce higher globular Kleene algebras with many compositions as well as domain and codomain operations, which generalize both modal Kleene algebras [J. Desharnais and G. Struth, Sci. Comput. Program. 76, No. 3, 181–203 (2011; Zbl 1211.68242)] and concurrent Kleene algebras [T. Hoare et al., J. Log. Algebr. Program. 80, No. 6, 266–296 (2011; Zbl 1278.68176)]. These generalized results are related to the point-wise approach to higher rewriting systems described by polygraphs. The principal contribution of this paper is the provision of a point-free algebraic approach to coherence in higher rewriting.
The synopsis of the paper goes as follows:

§ 2

introduces the relevant notions of higher rewriting, multifurcating into four subsections. §2.1 and §2.2 recall the definition of polygraphs and their properties as rewriting systems presenting higher categories. §2.3 introduces the notion of confluence filler for polygraphs with respect to cellular extensions, giving point-wise proofs of the coherent version of the Church-Rosser theorems and Newman’s lemma in the polygraph setting. §2.4 relates the confluence filler property to a more standard coherent confluence property [Y. Guiraud et al., Math. Z. 293, No. 1–2, 113–179 (2019; Zbl 1423.16008)].

§ 3

introduces higher globular Kleene algebras, multifurcating into three subsections. §3.1 lists the axioms of modal Kleene algebra [J. Desharnais and G. Struth, Sci. Comput. Program. 76, No. 3, 181–203 (2011; Zbl 1211.68242)], giving two of its main models. Its relational model provides the original intuition for defining modal operators based on relational domain and codomain operations over Kripke frames. Its path model, which can be defined over any graph, forms the basis for using modal Kleene algebras in higher rewriting. §3.2 defines \(n\)-dimensional dioids, rigging these in domain, codomain and star operations to obtain modal n-Kleene algebras. §3.3 constructs a higher path algebra associated to an \(n\)-polygraph with a cellular extension as a model of this structure.

§ 4

presents algebraic proofs of the coherent Church-Rosser theorem and Newman’s lemma in higher globular Kleene algebras multifurcating into three subsections. §4.1 first revisits abstract rewriting properties formulated in modal Kleene algebras [J. Desharnais et al., Log. Methods Comput. Sci. 7, No. 1, Paper No. 1, 29 p. (2011; Zbl 1214.68185); G. Struth, Lect. Notes Comput. Sci. 2561, 276–290 (2002; Zbl 1027.68071); J. Log. Algebr. Program. 66, No. 2, 239–270 (2006; Zbl 1086.68068)]. The authors then formalize notions from higher rewriting, introducing fillers in the setting of globular modal \(n\)-Kleene algebras, which correspond to the notion of fillers for polygraphs. They also define the notion of whiskering in modal \(n\)-Kleene algebras, describing the properties thereof. §4.2 esatablishes the coherent Church-Rosser theorem, first in Proposition 4.1 using classical induction and then in Theorem 4.2 using only the induction axioms for the Kleene star. §4.3 defines the notions of termination and well-foundedness for globular modal \(p\)-Boolean Kleene algebras, establishing Theorem 4.4, the coherent Newmann’s lemma.