Abstract. This paper investigates an approach to substitution alternative to the implicit treatment of the λ-calculus and the explicit treatment of explicit substitution calculi. ...
The third Termination Competition took place in June 2006. We present the background, results and conclusions of this competition. 1 Motivation and history In the past decades seve...
The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. ...
We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of λ-calculus by means of intersection type systems. The m...
We investigate garbage collection of unreachable parts of rooted graphs from a categorical point of view. First, we define this task as the right adjoint of an inclusion functor. ...