Higher-order logic programming

Dale A. Miller, Gopalan Nadathur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

68 Scopus citations


In this paper we consider the problem of extending Prolog to include predicate and function variables and typed λ-terms. For this purpose, we use a higher-order logic to describe a generalization to first-order Horn clauses. We show that this extension possesses certain desirable computational properties. Specifically, we show that the familiar operational and least fixpoint semantics can be given to these clauses. A language, λProlog that is based on this generalization is then presented, and several examples of its use are provided. We also discuss an interpreter for this language in which new sources of branching and backtracking must be accommodated. An experimental interpreter has been constructed for the language, and all the examples in this paper have been tested using it.

Original languageEnglish (US)
Title of host publication3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings
EditorsEhud Shapiro
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540164920
StatePublished - 1986
Event3rd International Conference on Logic Programming, ICLP 1986 - London, United Kingdom
Duration: Jul 14 1986Jul 18 1986

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume225 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other3rd International Conference on Logic Programming, ICLP 1986
Country/TerritoryUnited Kingdom

Bibliographical note

Funding Information:
This work has been supported by NSF grants MCS8219196-CER, MCS-82-07294, AI Center grants NSF-MCS-83-05221, US Army Research office grant ARO-DAA29-84-9-0027, and DARPA

Publisher Copyright:
© 1986, Springer-Verlag.


Dive into the research topics of 'Higher-order logic programming'. Together they form a unique fingerprint.

Cite this