Publications

My publications are available from the Computer Science department publications repository.

Areas of general interest for me are:

• term rewriting in various forms and guises
  
• expressiveness of programming language features, in particular
• expressiveness of type and module systems

Term Rewriting

In this area I have been specifically working in Infinitary Term Rewriting and Higher-Order Term Rewriting.

A seminal paper showing my way of thinking in Infinitary Rewriting is
Infinitary rewriting: meta-theory and convergence (this is a prelimary version for download; for publication details see here). This paper focuses on developing a meta-theory for infinitary term-rewriting by taking the topological foundations of the discipline a lot more seriously.

On the subject of termination for Higher-Order Rewriting, the paper Termination proofs in an Abstract Setting is an unpublished extended and corrected version of the RTA'95 paper mentioned on the publications page.

Expressiveness

One particular aspect of expressiveness I have looked at in recent years is expressiveness of typing features. For instance, I settled the problem that well-behaving untyped PCF programs can always be emulated by typed PCF programs. This work was presented at TLCA'03. The implementation for this can be found here.

Some recent unpublished work shows how one can implement type-safe red-black trees using Java generics. This is based on earlier work of a similar implementation of
red black trees in a functional setting. The difference is that the former implementation is in the style of GADTs, the latter uses some trickery involving nested types and phantom types.

Other Stuff

A little bit out of the ordinary is A Formalist's Perspective on Mathematics, a paper on the philosophy of mathematics. This just to show you what a twisted mind I have.

Research Interests

I belong to the following research groups:

• Programming Languages and Systems Group

My main interests are term rewriting, lambda-calculus and especially things that combine these, i.e. higher-order rewriting. 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.

In recent years I have been working on infinitary rewriting. The paper Infinitary Rewriting: Meta-theory and Convergence is an improved version of an earlier paper I had once put on this web page. The approach is solidly based on metric spaces and uses metric completion to a much wider extent than the standard literature deems appropriate.

The approach goes further in a number of ways: a general concept of term metric is defined, and it is studied under which conditions such term metrics are suitable for lifting relations from finite to infinitary terms. There are also restrictions on infinitary rewrite rules before they are regarded as acceptable; these are generalisations of the familiar condition that all variables on the right occur on the left. In a nutshell: the purpose of these conditions is to eliminate certain forms of non-convergence.

A more recent result of mine is that convergence is a modular property for non-collapsing iTRS, w.r.t. the standard term metric. My presentation for this result for RTA 2009, in powerpoint and pdf.

A few years ago, I had been experimenting with approaches to genetic programming, see for instance my RASC slides. This got me interested in issues about primitive recursion, and I proved 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.

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