Stefan Kahrs

Admin role - WAM Maintenance
+44 (0)1227 82 7146
 Stefan Kahrs


Outside CS I am a bit of a movie buff. Contributing lots of data to the IMDb I was one of its shareholders before it was sold to amazon. I also won the first Kevin Bacon challenge. My main area of expertise is the European exploitation cinema of the 1970s.

Research interests

I belong to the following research groups:

My main research interests are various flavours of 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.


Programming, theoretical computer science, algorithms.

Last updated