Metalinguistic features for formal parallel-program transformation

A set of metalinguistic features and their applications in formal parallel-program transformation are described. Program transformation is an effective methodology for developing correct and efficient parallel programs. However, manually carrying out the transformation is usually very cumbersome and error-prone. These metalinguistic features provide convenient language constructs for expressing and automating transformation steps. These features include a rationalized version of quoting and unquoting, a set a constructors, selectors, and predicates, and a collection of semantics preserving operators. The authors describe the metalinguistic features, illustrate how Crystal programs are conveniently manipulated with these meta constructs, and present a formal denotational semantics of the rationalized quoting and unquoting. They demonstrate the applications of these metalinguistic features by formally deriving a class of parallel palindrome recognition programs