Skip to main content

Research Repository

See what's under the surface

Advanced Search

Compiling concurrency correctly: cutting out the middle man

Hu, Liyang; Hutton, Graham

Authors

Liyang Hu



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.

Publication Date Sep 1, 2010
Publisher Intellect
Peer Reviewed Peer Reviewed
APA6 Citation Hu, L., & Hutton, G. (2010). Compiling concurrency correctly: cutting out the middle man
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
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

Files

concurrent.pdf (223 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations

;