Specification, transformation, and programming of concurrent systems in rewriting logic
Patrick D. Lincoln, Narciso Martı́-Oliet, José Meseguer · DIMACS series in discrete mathematics and theoretical computer science · 1994
This paper proposes a declarative paradigm in which parallelism is implicit and machine-independent, and the programs so developed are intrinsically parallel. This paradigm is obtained by generalizing the notion of rewriting to make it more widely applicable and capable of expressing not only functional computations but also a wide variety of parallel computations that are highly nonfunctional in nature. The generalization in question is provided by rewriting logic, a logic of change in which the states of a system are understood as algebraically axiomatized data structures, and the basic local changes that can concurrently occur in a system are axiomatized as rewrite rules that correspond to local patterns that, when present in the state of a system, can change into other patterns. Simple Maude, a carefully designed sublanguage of rewriting logic supporting three types of rewriting -- term, graph, and object-oriented --, is then proposed as a machine-independent parallel programming ...