  Partial evaluation (PE) is a powerful and general program optimization
technique with many successful applications. However, it has never been
investigated in the context of expressive rule-based languages like Maude,
CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with
sorts, subsorts and overloading; 2) equational rewriting modulo axioms such as
commutativity, associativity-commutativity, and
associativity-commutativity-identity. In this extended abstract, we illustrate
the key concepts by showing how they apply to partial evaluation of expressive
rule-based programs written in Maude. Our partial evaluation scheme is based on
an automatic unfolding algorithm that computes term variants and relies on
equational least general generalization for ensuring global termination. We
demonstrate the use of the resulting partial evaluator for program optimization
on several examples where it shows significant speed-ups.
