Metalevel computation in maude

Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way, and makes possible many advanced metaprogramming applications, including user-definable strategy languages, language extensions by new module composition operations, development of theorem proving tools, and reifications of other languages and logics within rewriting logic. A naive implementation of reflection can be computationally very expensive. We explain the semantic principles and implementation techniques through which efficient ways of performing reflective computations are achieved in Maude through its predefined META-LEVEL module.