Calculating correct compilers
In this article we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high- level semantics by systematic calculation, with all details of the implementation of the compilers falling...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Cambridge University Press
2015
|
| Online Access: | https://eprints.nottingham.ac.uk/32702/ |
| _version_ | 1848794470905020416 |
|---|---|
| author | Bahr, Patrick Hutton, Graham |
| author_facet | Bahr, Patrick Hutton, Graham |
| author_sort | Bahr, Patrick |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | In this article we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high- level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism, and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations. |
| first_indexed | 2025-11-14T19:16:43Z |
| format | Article |
| id | nottingham-32702 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:16:43Z |
| publishDate | 2015 |
| publisher | Cambridge University Press |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-327022020-05-04T17:16:59Z https://eprints.nottingham.ac.uk/32702/ Calculating correct compilers Bahr, Patrick Hutton, Graham In this article we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high- level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism, and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations. Cambridge University Press 2015-09-15 Article PeerReviewed Bahr, Patrick and Hutton, Graham (2015) Calculating correct compilers. Journal of Functional Programming, 25 (e14). pp. 1-47. ISSN 1469-7653 http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9961488&fileId=S0956796815000180 doi:10.1017/S0956796815000180 doi:10.1017/S0956796815000180 |
| spellingShingle | Bahr, Patrick Hutton, Graham Calculating correct compilers |
| title | Calculating correct compilers |
| title_full | Calculating correct compilers |
| title_fullStr | Calculating correct compilers |
| title_full_unstemmed | Calculating correct compilers |
| title_short | Calculating correct compilers |
| title_sort | calculating correct compilers |
| url | https://eprints.nottingham.ac.uk/32702/ https://eprints.nottingham.ac.uk/32702/ https://eprints.nottingham.ac.uk/32702/ |