  The logic programming paradigm provides the basis for a new intensional view
of higher-order notions. This view is realized primarily by employing the terms
of a typed lambda calculus as representational devices and by using a richer
form of unification for probing their structures. These additions have
important meta-programming applications but they also pose non-trivial
implementation problems. One issue concerns the machine representation of
lambda terms suitable to their intended use: an adequate encoding must
facilitate comparison operations over terms in addition to supporting the usual
reduction computation. Another aspect relates to the treatment of a unification
operation that has a branching character and that sometimes calls for the
delaying of the solution of unification problems. A final issue concerns the
execution of goals whose structures become apparent only in the course of
computation. These various problems are exposed in this paper and solutions to
them are described. A satisfactory representation for lambda terms is developed
by exploiting the nameless notation of de Bruijn as well as explicit encodings
of substitutions. Special mechanisms are molded into the structure of
traditional Prolog implementations to support branching in unification and
carrying of unification problems over other computation steps; a premium is
placed in this context on exploiting determinism and on emulating usual
first-order behaviour. An extended compilation model is presented that treats
higher-order unification and also handles dynamically emergent goals. The ideas
described here have been employed in the Teyjus implementation of the Lambda
Prolog language, a fact that is used to obtain a preliminary assessment of
their efficacy.
