Compiler correctness for parallel languages
Mitchell Wand · 1995
We present a paradigm for proving the correctness of compilers for languages with parallelism. The source language is given a denotational semantics as a compositional translation to a higher-order process calculus. The target language is also given a denotational semantics as a compositional translation to the same process calculus. We show the compiler is correct in that it preserves denotation up to bisimulation. The target language is also given an operational semantics, and this operational semantics is shown correct in the sense that it is branching-bisimilar to the denotational semantics of the target language. Together, these results show that for any program, the operational semantics of the target code is branching-bisimilar to the semantics of the source code. 1 Introduction In a series of papers in the early 80's [35, 34, 36, 12] we proposed a paradigm for semantics-based compiler correctness, and over the last several years we have begun putting this paradigm into practic...