[LC] ================================================ AMAST Links 02 03

                  Higher-Order Logic Programming
                by Gopalan Nadathur and Dale Miller

   "Higher-Order Logic Programming" can be obtained as an either
   DVI (?=dvi) or Postscript (?=ps) file respectively at URL: 
   ftp://cs.duke.edu/dist/papers/lprolog/holp.?.Z
  You can also use the WWW page URL:
   http://www.cis.upenn.edu/~dale/recent_papers.html
and trace the relevant links.

  This paper, which is to be a chapter in a handbook, provides an
exposition of the notion of higher-order logic programming. It begins
with an informal consideration of the nature of a higher-order
extension to usual logic programming languages. Such an extension is
then presented formally by outlining a suitable higher-order logic ---
Church's simple theory of types --- and by describing a version of
Horn clauses within this logic. Various proof-theoretic and
computational properties of these higher-order Horn clauses that are
relevant to their use in programming are observed. These observations
eventually permit the description of an actual higher-order logic
programming language. The applications of this language are
examined. It is shown, first of all, that the language supports
the forms of higher-order programming that are familiar from other
programming paradigms. The true novelty of the language, however, is
that it permits typed lambda terms to be used as data structures. This
feature leads to several important applications for the language in
the realm of meta-programming. Examples that bring out this
facet of the language are presented. A complete exploitation of
this meta-programming capability requires certain additional
abstraction mechanisms to be present in the language. This issue is
discussed, the logic of hereditary Harrop formulas is presented as a
means for realizing the needed strengthening of the language, and
the virtues of the features arising out the extension to the logic are
illustrated.