Compiling a 50-year journey
Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Cambridge University Press
2017
|
| Online Access: | https://eprints.nottingham.ac.uk/46962/ |
| _version_ | 1848797437693526016 |
|---|---|
| author | Hutton, Graham Bahr, Patrick |
| author_facet | Hutton, Graham Bahr, Patrick |
| author_sort | Hutton, Graham |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example in a modern context, and show how such a compiler can now be calculated directly from a specification of its correctness using simple equational reasoning techniques. |
| first_indexed | 2025-11-14T20:03:52Z |
| format | Article |
| id | nottingham-46962 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T20:03:52Z |
| publishDate | 2017 |
| publisher | Cambridge University Press |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-469622020-05-04T19:07:59Z https://eprints.nottingham.ac.uk/46962/ Compiling a 50-year journey Hutton, Graham Bahr, Patrick Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example in a modern context, and show how such a compiler can now be calculated directly from a specification of its correctness using simple equational reasoning techniques. Cambridge University Press 2017-09-20 Article PeerReviewed Hutton, Graham and Bahr, Patrick (2017) Compiling a 50-year journey. Journal of Functional Programming, 27 . e20/1-e20/11. ISSN 1469-7653 https://www.cambridge.org/core/journals/journal-of-functional-programming/article/compiling-a-50year-journey/31A66593E940CEF13253C34714F78041 |
| spellingShingle | Hutton, Graham Bahr, Patrick Compiling a 50-year journey |
| title | Compiling a 50-year journey |
| title_full | Compiling a 50-year journey |
| title_fullStr | Compiling a 50-year journey |
| title_full_unstemmed | Compiling a 50-year journey |
| title_short | Compiling a 50-year journey |
| title_sort | compiling a 50-year journey |
| url | https://eprints.nottingham.ac.uk/46962/ https://eprints.nottingham.ac.uk/46962/ |