Lecturer / Admissions Officer (Research)
My publications are available from the University of Kent's Academic Repository.Some selected publications:
Rewriting: closure operators, equivalences and models
(Acta Informatica 2013)
- Infinitary Term Rewriting: Foundations revisited; RTA 2010
- Modularity of Convergence in Infinitary Rewriting RTA 2009
Meta-Theory and convergence (Acta Informatica 2007)
I belong to the following research groups:term rewriting, e.g. infinitary rewriting, higher-order rewriting, as well as the first-order traditional stuff. These cover the whole range from implementations, proving properties about them, to semantic models. In recent years I have been specialising on infinitary rewriting, and on consistency proofs.
With infinitary rewriting one is trying to capture convergent behaviour of repeating computation, and to reason about it. In particular, I looked at the (surprisingly delicate) notion of equational reasoning about such computations, and its connection to semantic models.
Proving consistency of rewriting amounts to proving arbitrary non-trivial invariants. A consistency proof requires to define a suitable invariant, and then a semi-semantic setting in which such invariants can be established. We managed to get some positive results using finite coalgebras of a certain kind as the semi-semantic setting.
I am also interested in functional, logic, and functional-logic programming. The whole spectrum from questions about design, usage, expressiveness, type systems, methodology, specifications, semantics, down to things like implementation techniques, efficiency considerations etc. In other words, this is more or less the whole spectrum of what some people call Euro-Theory. One (unpublished) example of that is this proof that all primitive recursive functions can be enumerated without semantic duplicates. Sadly, this turned out to be a (not very well-) known result, proved by Ersov in the early 1970s.
Examples of random pieces of theory that caught my interest in recent years were red-black trees and regular expressions. I looked at variants of red-black trees, with various aims: employing a type-system to check the correctness of the balancing scheme was one, modifying invariants to permit tail-recursive or parent-free implmentations was another. For regular expressions, I looked at the problem to find (preferably) minimally-sized representatives of regular languages, for example to see how much alphabet-size influences the degree to which random regular expressions of certain sizes can be compressed.
Currently I am teaching Algorithms, Object-Oriented Programming, Logic Programming, Logic, and Regular Languages - listed in no particular order.
I actually prefer FP over OOP as a programming paradigm, partly because the programs tend to be much shorter, but mostly because OOP programs are nigh impossible to reason about.
Currently my main admin job is examinations officer.
Occasionally, just occasionally I actually do write the odd little program. For example, some time of summer 1999 I spent writing an applet for the translation of regular expressions. Note the input alphabet are all alphanumeric characters, iteration is * (and +), choice is |, epsilon is %, the empty language is @, and parentheses are for grouping. After entering the input regexp (in the text field - do not forget to finish it with RETURN), the graph is transformed stepwise by continually pressing the transform button.
Being a screwed-up scientist, I obviously tried to give this piece of work the scientific treatment. One could argue though that collecting and analysing transformation rules for regular expressions from the literature is closer to trainspotting than doing science...