Maude
A reflective 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 universal. 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 meta-module, 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).
- The home page, moved from SRI to UIUC.
- The Maude Manual.
- Some Papers on Maude and Rewriting Logic.
- A course using Maude to analyze distributed systems with example Maude code and a tutorial on Maude.
- Another course using Maude has a few tutorials.
- An XEmacs editing and interaction mode.
- MobileMaude - A prototype of a Mobile Maude system, written by Carolyn Talcott, it is very similar to the Tube
- Real-Time Maude - A programming language and tool, based on Maude, supporting the formal specification and analysis of real-time and hybrid systems, with an execution environment for a real-time extension of the Actor model
- Reflection in Maude - About reflection in Maude: Talk about the universal rewrite theory, how this is used to model and operate any inference system, the quotation system, the meta-level modules defined, and how to modify and extend them
- Syntax in Maude - About syntax in Maude: from the parsing section (se below) in the Maude manual can be had many insights about Maude's syntax and the reasoning behind it
Pages in this topic: MobileMaude Real-Time Maude Reflection in Maude Syntax in Maude
Also linked from: ADATE Algebraic Specification CafeOBJ José Meseguer Metalogical Reflection Methods of Reflection Rewrite Logic 101 Sprint Tactic Trotskyite Tunes