Compiling concurrency correctly: cutting out the middle man
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 establis...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
Intellect
2010
|
| Online Access: | https://eprints.nottingham.ac.uk/28187/ |
| _version_ | 1848793521587224576 |
|---|---|
| author | Hu, Liyang Hutton, Graham |
| author_facet | Hu, Liyang Hutton, Graham |
| author_sort | Hu, Liyang |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T19:01:37Z |
| format | Conference or Workshop Item |
| id | nottingham-28187 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:01:37Z |
| publishDate | 2010 |
| publisher | Intellect |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-281872020-05-04T20:24:51Z https://eprints.nottingham.ac.uk/28187/ Compiling concurrency correctly: cutting out the middle man Hu, Liyang Hutton, Graham 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. Intellect 2010-09 Conference or Workshop Item PeerReviewed Hu, Liyang and Hutton, Graham (2010) Compiling concurrency correctly: cutting out the middle man. In: Symposium on Trends in Functional Programming (10th), 2-4 June 2009, Komárno, Slovakia. |
| spellingShingle | Hu, Liyang Hutton, Graham Compiling concurrency correctly: cutting out the middle man |
| title | Compiling concurrency correctly: cutting out the middle man |
| title_full | Compiling concurrency correctly: cutting out the middle man |
| title_fullStr | Compiling concurrency correctly: cutting out the middle man |
| title_full_unstemmed | Compiling concurrency correctly: cutting out the middle man |
| title_short | Compiling concurrency correctly: cutting out the middle man |
| title_sort | compiling concurrency correctly: cutting out the middle man |
| url | https://eprints.nottingham.ac.uk/28187/ |