Kernel-LEAF: A logic plus functional language

Kernel-LEAF is a logic plus functional language based on the flattening technique. It differs from other similar languages because it is able to cope with partial (undefined or non-terminating) functions. This is achieved by introducing the distinction between data structures and (functional) term structures, and by using two kinds of equality. The language has a clean model-theoretic semantics, where the domains of the interpretations are the algebraic CPOs. In these domains the difference between the two equalities corresponds to a different behaviour with respect to continuity. The operational semantics (based on SLD-resolution) is proved sound and complete with respect to the model-theoretic one. Finally, an outermost strategy, more efficient than unrestricted SLD-resolution, but still complete, is presented.