Rewriting logic expresses an essential equivalence between logic and computation. System states are in bijective correspondence with formulas and concurrent computations are in bijective correspondence with proofs. Given this equivalence between computation and logic, a rewriting logic axiom of the form t --> t' has two readings. omputationally, it means that a fragment of a system's state that is an instance of the pattern t can change to the corresponding instance of t' concurrently with any other state changes; logically, it just means that we can derive the formula t' from the formula t. Rewriting logic is entirely neutral about the structure and properties of the formulas/states t. They are entirely user-definable as an algebraic data type satisfying certain equational axioms. Because of this ecumenical neutrality, rewriting logic has, from a logical viewpoint, good properties as a logical framework, in which many other logics can be naturally represented. And, computationally, it has also good properties as a semantic framework, in which many different system styles and models of concurrent computation and many different languages can be naturally expressed without any distorting encodings. The goal of this paper is to provide a relatively gentle introduction to rewriting logic, and to paint in broad strokes the main research directions that, since its introduction in 1990, have been pursued by a growing number of researchers in Europe, the US, and Japan. Key theoretical developments, as well as the main current applications of rewriting logic as a logical and semantic framework, and the work on formal reasoning to prove properties of specifications are surveyed.
(BibTeX entry) (gzip'ed Postscript)