A _(reflective|reflection) equational *(rewrite) *(logic) *(programming language) in the _(OBJ) family of executable specification languages.

Maude programs consist of modules which specify a set of term types, equations that should hold within the module over those types along with some annotations, and declarations that explain what manner of relations (such as importing) the module has with other modules. The equational reductions that Maude specifies are _(concurrent) in that they can be applied in any order.

However, Maude is even more interesting because the rewriting theory that it uses is <em>universal</em>. That is, it can express the reduction strategy of any other logic, including itself. The way this is done is that the default reduction strategy is contained within the strategy <em>meta-module</em>, and there can be further such modules that provide modified forms of it. Maude's (relatively complicated) form of expression quotation allows the possibility of modifying this in small ways without the full overhead of a static meta-module specification. This means that "backtracking" and other procedural hacks in logical languages are avoided in favor of a direct manipulation of the language as needed, so it will most often be totally transparent to the program (which is a specification, so this is important to keep out the "how" elements).

<ul class="links">
<li>The _(home page|http://maude.cs.uiuc.edu), moved from SRI to UIUC.
<li>The _(Maude Online Manual| http://maude.cs.uiuc.edu/manual/maude-manual-html/).
<li>_(Some Papers on Maude and Rewriting Logic| http://www.csl.sri.com/users/duran/).
</ul>