All applications typical of equational programming and algebraic specification can be conveniently and efficiently supported through Maude's sublanguage of functional modules. In fact, the paper [41] argues that Maude's equational logic, namely, membership equational logic, is so expressive--yet efficiently implementable--as to offer very good advantages as a logical framework for a very wide range of algebraic specification languages based on both total and partial equational logic formalisms.
However, many other Maude applications go beyond equational logic. System modules support general rewriting logic applications. The important area of concurrent and distributed object-based system specification and prototyping is supported by object-oriented modules. And reflection makes possible many novel metaprogramming and metalanguage applications. In particular, reflection is extremely valuable in many applications using rewriting logic as a logical and semantic framework. Thanks to the sustained efforts of many researchers, particularly in the ELAN, Pisa, Stanford, and Maude teams, there is by now very extensive evidence supporting the claim that rewriting logic is indeed a very flexible and simple semantic framework [37, 40, 42, 6], and logical framework [32, 29, 62, 30, 2, 55, 8, 16, 10, 12]. Moreover, object-oriented design languages, architectural description languages, and languages for distributed components also have a natural semantics in rewriting logic [63, 34, 57, 47, 48] (see Section 2.8.2 for more discussion on the use of reflection in logical and semantic framework applications, and Appendix E for an application of Maude to the interoperation of software architectures).
The largest Maude application developed so far is Full Maude itself [19] (about 7,000 lines of Maude code). Two other substantial applications are an inductive theorem prover and a Church-Rosser checker for equational theories, that are part of a formal environment for Maude and for the CafeOBJ language [12]. In addition, several language interpreters and strategy languages, a supercompiler, several object-oriented specifications--including cryptographic protocols and network applications--and a variety of executable translations mapping logics, architectural description languages and models of computation into the rewriting logic reflective framework have been developed by different authors (see references in [20, 42, 28]). We hope that the present release will encourage and support many other applications.