  Many functional logic languages are based on narrowing, a unification-based
goal-solving mechanism which subsumes the reduction mechanism of functional
languages and the resolution principle of logic languages. Needed narrowing is
an optimal evaluation strategy which constitutes the basis of modern
(narrowing-based) lazy functional logic languages. In this work, we present the
fundamentals of partial evaluation in such languages. We provide correctness
results for partial evaluation based on needed narrowing and show that the nice
properties of this strategy are essential for the specialization process. In
particular, the structure of the original program is preserved by partial
evaluation and, thus, the same evaluation strategy can be applied for the
execution of specialized programs. This is in contrast to other partial
evaluation schemes for lazy functional logic programs which may change the
program structure in a negative way. Recent proposals for the partial
evaluation of declarative multi-paradigm programs use (some form of) needed
narrowing to perform computations at partial evaluation time. Therefore, our
results constitute the basis for the correctness of such partial evaluators.
