Compiling concurrency correctly: cutting out the middle man
Liyang Hu, Graham Hutton · 2010
Abstract The standard approach [23] to proving compiler correctness for concurrent languages requires the use of multiple translations into an intermediate process calculus. We present a simpler approach that avoids the need for such an intermediate language, using a new method that allows us to directly establish a bisimulation between the source and target languages. We illustrate the technique on two small languages, using the Agda system to present and formally verify our compiler correctness proofs. 1.1