By Gopalan Nadathur and Dale Miller, from ICLP 88, available from the λProlog website:
λProlog is a logic programming language that extends Prolog by incorporating notions of higher-order functions, λ-terms, higher-order unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical first-order theory of Horn clauses to the intuitionistic higher-order theory of hereditary Harrop formulas. The justification for considering this extension a satisfactory logic programming language is provided through the proof-theoretic notion of a uniform proof. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various aspects of an experimental implementation of λProlog.
EDIT: Teyjus 2.0 is available.