Georg
STRUTH

PROJECT

Algebraic Coherence, Higher-Dimensional Kleene Algebras and Interactive Theorem Proving

Kleene algebras were originally developed to reason about computing systems and have recently been generalised to model higher-dimensional rewriting systems in mathematics. The aim of this project is to develop further variants of these algebra to verify coherence properties in categorical algebra. In support of this it seems essential to formalise the approach with proof assistants to manage the inherent combinatorial complexity of reasoning with higher categories.
The project emphasises in particular applications of the algebras in geometric approaches to concurrent and distributed computing systems. Operationally, the algebras are meant to provide a further layer of abstraction suitable for equational reasoning about categorical diagrams and for encoding reduction strategies, and to be amenable to proof automation and algorithmic treatment.
The results envisaged will therefore be novel higher dimensional Kleene algebras (with globular, (pre)cubical and simplicial variants), algebraic coherence proofs for higher-dimensional algebras, a formalisation of the approach in a proof assistant such as Coq or Isabelle, and its application in concurrency, especially with higher-dimensional automata.
The work proposed is a collaboration with Philippe Malbos and Damien Pous, involving further researchers at Lyon, Paris and Sheffield.

BIOGRAPHY

Georg Struth is full professor of theoretical computer science at the University of Sheffield, UK, and head of its verification group. He has a longstanding track record on algebras and logics for programs, program semantics and verification, and formalised mathematics with interactive proof assistants. He is best known for his pioneering work
on theory and applications of Kleene algebras and quantales; from axiomatic extensions such as modal, concurrent, cylindric variants, completeness and decidability questions to application in program correctness and the design of verification tools. Some more recent work has focused on quantitative verification, semantics for probabilistic and hybrid systems (where continuous dynamical systems interact with discrete control), and on geometric models of distribution and concurrency using higher-dimensional rewriting with polygraphs as well as higher-dimensional automata.

BIBLIOGRAPHY

1. G. Struth Trimming the Hedges: An Algebra to Tame Concurrency, in C.Jones and J. Misra, Theory of Programming: Life and Work of Tony Hoare,Turing Award Series, Association of Computing Machinery, 2021.
2. B. Dongol, I. J. Hayes and G. Struth. Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras, Logical Methods in Computer Science 17(1), 2021.
3. J. Huerta y Munive and G. Struth. Verifying Hybrid Systems with Modal Kleene Algebra. RAMiCS 2018, volume 11194 of LNCS, pages 225–243, Springer, 2018.
4. A. Armstrong, V. B. F. Gomes and G. Struth . Building Program Construction and Verification Tools from Algebraic Principles, Formal Aspects of Computing, 28(2): 265–293, 2016.
5. H. Furusawa and G. Struth. Concurrent Dynamic Algebra, ACM Transactions on Computational Logic, 16(4): 30, 2015.
6. M. R. Laurence and G. Struth. Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages. RAMiCS 2014, volume 8428 of LNCS, pages 65–82, Springer, 2014.
7. C. A. R. Hoare, B. Möller, G. Struth and I. Wehrman. Concurrent Kleene Algebra and its Foundations, Journal of Logic and Algebraic Programming 80(6):266–296, 2011.
8. J. Desharnais and G. Struth. Internal Axioms for Domain Semirings, Science of Computer Programming 76(3):181–203, 2011.
9. C. A. R. Hoare, A. Hussain, B. Möller, P. W. O’Hearn, R. L. Peterson and G. Struth. On Locality and the Exchange Law for Concurrent Processes. CONCUR 2011, volume 6901 of LNCS, pages 250–264. Springer, 2011.
10. J. Desharnais, B. Möller, and G. Struth. Kleene algebra with domain. ACM Transactions on Computational Logic, 7(4):798–833, 2006.