A truly concurrent semantics for the double-struck K framework based on graph transformations

Abstract

This paper gives a truly concurrent semantics with sharing of resources for the semantic framework, an executable (term-)rewriting-based formalism for defining programming languages and calculi. Akin to graph rewriting rules, the (rewrite) rules explicitly state what can be concurrently shared with other rules. The desired true concurrency is obtained by translating the rules into a novel instance of term-graph rewriting with explicit sharing, and then using classical concurrency results from the double-pushout (DPO) approach to graph rewriting. The resulting parallel term-rewriting relation is proved sound, complete, and serializable with respect to the jungle rewriting flavor of term-graph rewriting, and, therefore, also to term rewriting. © 2012 Springer-Verlag.