[Prev][Next][Index][Thread]

Higher-Order Logic Programming



This message is to announce the availability of the paper

   Higher-Order Logic Programming

by Dale Miller and myself. This paper should be of interest to
subscribers to the types mailing list because it describes the use of
Church's Simple Theory of Types --- a type-theoretic language --- as a
means for programming. An abtract is enclosed at the end of the message.

The paper can be obtained by anonymous ftp from cs.duke.edu. It is
present in (compressed) dvi and ps forms in 

~ftp/dist/papers/lprolog/holp.{dvi,ps}.Z 

The WWW path to these files is 

ftp://cs.duke.edu/dist/papers/lprolog/holp.{dvi,ps}.Z

You can also use the URL 

http://www.cis.upenn.edu/~dale/recent_papers.html

and trace the relevant links.

-Gopalan Nadathur

-----------------------------

Higher-Order Logic Programming

Gopalan Nadathur and Dale Miller


Abstract:

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.