Implementation of Higher-Order Unification Based on Calculus of Explicit Substitution

. In this paper, we present several improvements of an algorithm for a higher-order unification based on the calculus of explicit substitutions. The main difference between our algorithm and the already known version is, that we try to postpone normalisation of oe-terms as long as possible, i.e. until some information of these oe-terms is necessary for the next step of the unification algorithm. 1 Introduction In this paper, we describe an improved version of a higher-order unification algorithm, which was presented in [DHK95]. The main idea of this algorithm is based on a calculus of explicit substitutions in a simply typed -theory (for definitions and details, see [ACCL90]), which integrates substitutions in the framework of the first-order formalism. In this calculus, substitutions are treated as the firstorder objects, i.e. all basic operations over substitutions, like an application, a composition and a concatenation are defined in the first-order theory (their semantic is descri..