Title
From Hyperedge Replacement to Separation Logic and Back
Abstract
Hyperedge-replacement grammars and separation-logic formulas both define classes of graph-like structures. In this paper, we relate the different for- malisms by effectively translating restricted hyperedge-replacement grammars into formulas of a fragment of separation-logic with recursive predicates, and vice versa. The translations preserve the classes of specified graphs, and hence the two ap- proaches are of equivalent power. It follows that our fragment of separation-logic inherits properties of hyperedge-replacement grammars, such as inexpressibility re- sults. We also show that several operators of full separation logic cannot be ex- pressed using hyperedge replacement.
Year
Venue
Keywords
2008
ECEASST
graph grammars,program verification,graph transformation,separation logic,hyperedge replacement
Field
DocType
Volume
Rule-based machine translation,Tree-adjoining grammar,Discrete mathematics,Separation logic,L-attributed grammar,Programming language,Computer science,Theoretical computer science,Operator (computer programming),Predicate (grammar),Rotation formalisms in three dimensions,Recursion
Journal
16
Citations 
PageRank 
References 
4
0.39
4
Authors
2
Name
Order
Citations
PageRank
Mike Dodds116910.70
Detlef Plump260462.14