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)