Two-level approach to logic and functional programming

This paper presents an approach to the integration of two declarative programming styles, namely logic programming, as supported by the Prolog language, and higher-order functional programming, as available in languages like ML, Miranda, and LISP. The integration is obtained by adopting, as a high level intermediate language, a well founded first order logic language with equality, K-LEAF, for which an efficient computational model has been already developed, based on resolution and suited to Prolog-like implementation. The compilation of the highly-expressive higher-order user language IDEAL to K-LEAF can be represented by a formal deduction of universal properties of actual programs an axiomatization of a version of lambda-reduction, expressed in K-LEAF. The efficiency obtainable is of the same order of commercially available LISP systems.