| Autor: |
Cameron Calk, Eric Goubault, Philippe Malbos, Georg Struth |
| Jazyk: |
angličtina |
| Rok vydání: |
2022 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Vol Volume 18, Issue 4 (2022) |
| Druh dokumentu: |
article |
| ISSN: |
1860-5974 |
| DOI: |
10.46298/lmcs-18(4:9)2022 |
| Popis: |
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. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
