Liyang on the intartubes

Compiling Concurrency Correctly: Cutting Out the Middle Man

Liyang HU and Graham Hutton. Submitted to the Symposium on Trends in Functional Programming, 2009.

The standard approach to proving compiler correctness for concurrent languages requires the use of multiple trans­la­tions into an intermediate process calculus. We present a simpler approach that avoids the need for such an in­ter­me­di­ate language, using a new method that allows us to di­rect­ly establish a bisimulation between the source and target lan­gua­ges. We illustrate the technique on two small lan­gua­ges, using the Agda system to present and formally verify our com­piler correctness proofs.

[Paper^†] [Slides] [Proofs^‡] [BibTeX]