School of Computing

Stefan Kahrs

Lecturer / Exams Officer

Photo of Stefan Kahrs, if available
  • Room SW105
    School of Computing
    University of Kent,
    CT2 7NF


My publications are available from the University of Kent's Academic Repository.

Some selected publications:

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.


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.

Other CS

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, which no longer runs, because browsers hate Java, even appletviewer hates it now.

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...

And now for something completely different

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.

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 06/08/2020