Abstract Narrowing-driven partial evaluation (NPE) is a powerful specialization technique for rewrite systems, i.e., for the first-order component of many functional (logic) languages like Haskell, Curry or Toy. Partial evaluators fall in two main categories, online and offline, according to the time when termination issues are addressed. Online partial evaluators are usually more precise since more information is available. For instance, the original NPE scheme (which follows the online approach) considers a variant of the Kruskal tree condition called "homeomorphic embedding" [Leuschel 2002] to ensure the termination of the process: if a term embeds some previous term in the same narrowing computation, some form of generalization---usually the most specific generalization operator---is applied and partial evaluation is restarted with the generalized terms. However, this extra precision comes at a cost: the homeomorphic embedding tests, together with the associated generalizations, make NPE very expensive and, thus, it does not scale up well to realistic problems like interpreter specialization. Offline partial evaluators usually proceed in two stages: the first stage returns a program that includes annotations to guide the partial computations (e.g., to identify those function calls that can be safely unfolded); then, the second stage---the proper partial evaluation---only needs to obey the annotations and, thus, it is generally much faster than online partial evaluators. In this thesis we present a more efficient narrowing-driven partial evaluation scheme that ensures termination by following the offline approach. For this, we identify a class of quasi-terminating rewrite systems, called nonincreasing. In such programs, only finitely many different terms---modulo variable renaming---are computed by needed narrowing. This is an important property since quasi-termination of programs is frequently a sufficient condition to ensure the termination of the specialization process. Unfortunately, this class is too restrictive and, thus, we also introduce an algorithm that takes an inductively sequential program (a much broader class of programs for which NPE is originally defined) and annotates those expressions that violate nonincreasing characterization. Then, we define an extended needed narrowing relation: generalizing needed narrowing, in which annotated subterms are generalized. Once the new partial evaluation method is defined, we develop an offline narrowing-driven partial evaluator prototype. Its experimental validation demonstrates that the offline scheme is faster than the online approach. Recently, a new principle for termination analysis of programs was formulated. The principle is based on the size change of arguments at function calls: size-change graphs. Since size-change graphs were originally introduced for functional languages, we adapt the formalism to functional logic programs. Size-change graphs are useful to detect a specific form of quasi-termination, which is used to make annotations analogously to our first offline approximation. This allows us to improve the precision of the annotation phase. One important partial evaluation challenge is the specialization of realistic applications. Domain Specific Embedded Languages (DSELs) produce inefficient code due to the interpretation overhead. This is the reason why [Hudak 1998, Seefried et al. 2004, Christensen 2003] propose partial evaluation in order to overcome this drawback. We select the routers domain, in particular we choose the Click software router model and develop a language for router specification embedded in Curry: Rose. Finally, the development of Rose was also useful to test the pros and cons of Curry in the DSEL area. It was also useful to check the power of the partial evaluation scheme in order to compile programs by using the NPE technique.