Algebra of Computing
In this project 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 (Cambridge). Our joint work applies the theory to perform automated reasoning about computing systems.
- Algebras for Iteration and Infinite Computations (Isabelle theory describing iterations and computation models with aborting, finite and infinite executions)
- 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)
- Isabelle repository for relational and algebraic methods (Georg Struth's page)
General correctness: algebraic foundations and mechanisation
DAAD Postdoc fellowship as visiting researcher at the University of Sheffield, April 2010 - March 2011
- Extended Designs Algebraically, SCP 78(11):2064-2085, 2013
- Unifying Lazy and Strict Computations, 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, MPC 2012
- Automating Algebraic Methods in Isabelle (with G. Struth, T. Weber), ICFEM 2011
- Fixpoints for General Correctness, JLAP 80(6):248-265, 2011
- A Repository for Tarski-Kleene Algebras (with G. Struth, T. Weber), ATE 2011
- Towards a Typed Omega Algebra, RAMiCS 2011
- Unifying Recursion in Partial, Total and General Correctness, UTP 2010
- Partial, Total and General Correctness, MPC 2010
- General Correctness Algebra, RelMiCS/AKA 2009
- ... all publications