Higher-Order Logic Programming as Constraint Logic Programming.
Spiro Michaylov, Frank Pfenning · 1993
Higher-order logic programming (HOLP) languages are particularly useful for various kinds of metaprogramming and theorem proving tasks because of the logical support for variable binding via - abstraction. They have been used for a wide range of applications including theorem proving, programming language interpretation, type inference, compilation, and natural language parsing. Despite their utility, current language implementations have acquired a well-deserved reputation for being inefficient. In this paper we argue that HOLP languages can reasonably be viewed as Constraint Logic Programming (CLP) languages, and show how this can be expected to lead to more practical implementations by applying the known principles for the design and implementation of practical CLP systems. 1 Introduction Higher-order logic programming (HOLP) languages [17] typically use a typed -calculus as their domain of computation. In the case of Prolog [18] it is the simply-typed -calculus, while in the case...