Compiling concurrency correctly: cutting out the middle man

Hu, Liyang; Hutton, Graham

Abstract

The standard approach 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.

Citation

Hu, L., & Hutton, G. Compiling concurrency correctly: cutting out the middle man. Presented at Symposium on Trends in Functional Programming (10th)

• Conference Name: Symposium on Trends in Functional Programming (10th)
• End Date: Jun 4, 2009
• Publication Date: Sep 1, 2010
• Deposit Date: Mar 18, 2015
• Publicly Available Date: Mar 18, 2015
• Publisher: Intellect
• Peer Reviewed: Peer Reviewed
• Public URL: https://nottingham-repository.worktribe.com/output/1011754
• Additional Information: Selected papers from the Tenth Symposium on Trends in Functional Programming, Komarno, Slovakia, June 2009.; ; Published in: Trends in functional programming. Vol. 10. Bristol : Intellect, 2011, ISBN: 9781841504056. pp. 17-32