| Year | 2012 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Traian Serbanuta, Grigore Rosu |
Links
Abstract
This paper gives a truly concurrent semantics with sharing of resources for the K semantic framework, an executable (term-) rewriting-based formalism for defining programming languages and calculi.
Akin to graph rewriting rules, the K (rewrite) rules explicitly state what can be concurrently shared with other rules.
The desired true concurrency is obtained by translating the K 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.