Department of Computer Science
The University of Sheffield
Regent Court, 211 Portobello Street
Sheffield S1 4DP, UK
Tel: +44 (0)114 22 21846
Fax: +44 (0)114 22 21810
- Models and calculi for software systems and programming languages
- Formal development and analysis of systems
- Computational algebras, lattice theory, Kleene algebra
- Logic in computer science, mechanised and automated reasoning
- Term rewriting, decision procedures, complexity
- Abstract Abstract Reduction. Journal of Logic and Algebraic Programming. pdf. (to appear)
- Kleene Algebra with Domain, with Jules Desharnais and Bernhard Möller. ACM TOCL. pdf. (to appear)
- Modal Kleene Algebra and Partial Correctness, with Bernhard Möller. AMAST 2004. pdf (best paper award).
- A Calculus for Set-Based Program Development. ICFEM 2003. postscript.
- Deriving Focused Calculi for Transitive Relations. RTA 2001. postscript.
- An Algebra of Resolution. RTA 2000.
Mechanised Algebraic Reasoning
The following links lead to web sites with mechanised and automated
proofs in algebraic structures.
Theorem Proving (slides from a lecture series at the Midlands Graduate School
Algebraic Methods (slides from a lecture series at the Midlands Graduate School 2008)