The intent of this article is twofold: To survey prominent proposals for the integration of logic and functional programming and to present a new paradigm for the same purpose. We categorize current research into four types of approaches, depending on the level at which the proposed integration is achieved. Unlike most current work, our approach is not based on extending unification to general-purpose equation solving. Rather, we propose a computation delaying mechanism calledresiduation. This allows a clear distinction between functionalevaluation and logicaldeduction. The former is based on theλ-calculus, and the latter on Horn clause resolution. Residuation is built into the unification operation which may then account forβ-reduction. In clear contrast with equation-solving approaches, our model supports higher-order function evaluation and efficient compilation of both functional and logic programming expressions, without being plagued by non-deterministic term-rewriting. In addition, residuation lends itself naturally to process synchronization and constrained search. We describe an operational semantics and an implementation of a prototype language called LeFun—Logic, equations, and Functions.