Metalevel Computation in Maude

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, and José Meseguer

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.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International