A Higher Order Rewriting Logic for Functional Logic Programming.

According to a well known conception, programs in a declarative programming language can be viewed as theories in some suitable logic, while computations can be viewed as deductions. In our opinion, there is yet no general assent on the logic to be viewed as the foundation of higher order, lazy functional logic languages. In this paper, we argue that a specific rewriting logic can play this role, and we justify the adequacy of our proposal by means of proof-theoretical and model-theoretical results. Moreover, we present a sound and complete lazy narrowing calculus for goal solving, and we discuss a circuit synthesis problem that illustrates the expressiveness of our approach. This example has been tested in an implemented system.