This paper studies the calculus X, that has its foundation in Classical Logic; we present an implementation for X using term graph rewriting techniques, and discuss improvements thereof which result in an increasingly more efficient running of the reduction engine.
We show that name capture can be dealt with `on the fly', by realising the avoidance of capture through adding or modifying the rewrite rules.
We study two different approaches to garbage collection, and compare the various implementations by presenting benchmarks.