Algebra of computing
Please see the main page for contact, research and teaching information.
In this research I devise algebraic descriptions of computation models for sequential systems. A particular aim is to structure and unify the diversity of models described in the literature. To this end, I give axioms for key aspects of the models, for example, the infinite executions of a computation.
- Some axioms are common to many models and frequently suffice to derive complex results, for example, program transformations and refinement rules for program development.
- Individual models are characterised by adding specific axioms to the common ones, so that the resulting theories and methods specialise in various ways useful for different application areas.
According to the assumed axioms, the models are organised in a hierarchy of algebraic structures, the algebras of computing.
The theories are described by first-order axioms and ideally suited for support by automated theorem provers and SMT solvers. I implement them in Isabelle based on algebraic theories developed jointly with Georg Struth (Sheffield) and Tjark Weber (Uppsala). Our joint work applies the theory to perform automated reasoning about computing systems.
In recent work I am applying algebraic methods to verify the correctness of graph algorithms.
The following Isabelle theories are the basis of my most recent publications:
- Algebras for Correctness of Sequential Computations (Isabelle theory uniformly describing preconditions, correctness statements and calculi for sequential computation models including monotonic Boolean transformers which need a theory with Lattice properties; as PDF)
- Algebras for Iteration and Infinite Computations (Isabelle theory describing iterations and computation models with aborting, finite and infinite executions)
- An Algebraic Approach to Computations with Progress (Isabelle theory describing algebras for computations with progress such as passing of time or traces getting longer; as PDF)
- An Algebraic Approach to Multirelations and their Properties (Isabelle theory describing algebras of multirelations; as PDF)
- An Algebraic Framework for Minimum Spanning Tree Problems (ZIP file with Isabelle2016-1 theories proving the correctness of Prim's minimum spanning tree algorithm based on algebras for aggregation; presented in four documents: Stone Algebras (PDF) and Stone Relation Algebras (PDF) and Stone-Kleene Relation Algebras (PDF) and An Algebraic Framework for Minimum Spanning Tree Problems (PDF))
- Closure, Properties and Closure Properties of Multirelations (Isabelle theory describing algebras of multirelations; as PDF)
- Infinite Executions of Lazy and Strict Computations (Isabelle theory uniformly describing infinite executions, recursion and iteration in strict and non-strict computation models; as PDF)
- Relation-Algebraic Verification of Prim's Minimum Spanning Tree Algorithm (ZIP file with Isabelle theories proving the correctness of Prim's minimum spanning tree algorithm; as PDF)
- Stone Relation Algebras (ZIP file with Isabelle2016 theories generalising relation algebras to the weighted-graph model; presented in three documents: Stone Algebras (link to AFP) and Stone Relation Algebras (PDF) and Stone-Kleene Relation Algebras (PDF))
- Unifying Correctness Statements (Isabelle theory uniformly describing preconditions, correctness statements and calculi for various sequential computation models; as PDF)
- Unifying Lazy and Strict Computations (Isabelle theory giving a unified semantics to recursion and iteration in strict and non-strict computation models; as PDF)
- A technical report with consolidated Isabelle theories from my research until 2015
- Isabelle repository for relational and algebraic methods (Georg Struth's page)
- Algebras of multirelations for modelling interaction and cooperation
JSPS Invitation Fellowship for Research in Japan, 2015
- General correctness: algebraic foundations and mechanisation
DAAD Postdoc fellowship as visiting researcher at the University of Sheffield, 2010-2011
- ... all publications
- Stone Relation Algebras, RAMiCS 2017, to appear
- An Algebraic Approach to Multirelations and their Properties (with R. Berghammer), JLAMP, 88:45-63, 2017
- Stone Relation Algebras, AFP, 2017
- Relation-algebraic verification of Prim's minimum spanning tree algorithm, LNCS 9965:51-68, ICTAC 2016
- Stone Algebras, AFP, 2016
- An Algebraic Approach to Computations with Progress, JLAMP 85(4):520-539, 2016
- Kleene Algebras with Domain (with V. B. F. Gomes, P. Höfner, G. Struth, T. Weber), AFP, 2016
- Closure, Properties and Closure Properties of Multirelations (with R. Berghammer), LNCS 9348:67-83, RAMiCS 2015
- A Relation-Algebraic Approach to Multirelations and Predicate Transformers (with R. Berghammer), LNCS 9129:50-70, MPC 2015
- Infinite executions of lazy and strict computations, JLAMP 84(3):326-340, 2015
- Algebras for Correctness of Sequential Computations, SCP 85(B):224-240, 2014
- Extended Conscriptions Algebraically, LNCS 8428:139-156, RAMiCS 2014
- Multirelations with Infinite Computations, JLAMP 83(2):194-211, 2014
- Extended Designs Algebraically, SCP 78(11):2064-2085, 2013
- Unifying Lazy and Strict Computations, LNCS 7560:17-32, RAMiCS 2012
- Algebras for Iteration and Infinite Computations, Acta Informatica 49(5):343-359, 2012
- Typing Theorems of Omega Algebra, JLAP 81(6):643-659, 2012
- Unifying Correctness Statements, LNCS 7342:198-219, MPC 2012
- Automating Algebraic Methods in Isabelle (with G. Struth, T. Weber), LNCS 6991:617-632, ICFEM 2011
- Fixpoints for General Correctness, JLAP 80(6):248-265, 2011
- A Repository for Tarski-Kleene Algebras (with G. Struth, T. Weber), CEUR-WS 760:30-39, ATE 2011
- Towards a Typed Omega Algebra, LNCS 6663:196-211, RAMiCS 2011
- Unifying Recursion in Partial, Total and General Correctness, LNCS 6445:207-225, UTP 2010
- Partial, Total and General Correctness, LNCS 6120:157-177, MPC 2010
- General Correctness Algebra, LNCS 5827:150-165, RelMiCS/AKA 2009