Compiling a 50-year journey

Hutton, Graham; Bahr, Patrick

Abstract

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.

Citation

Hutton, G., & Bahr, P. (2017). Compiling a 50-year journey. Journal of Functional Programming, 27, Article e20. https://doi.org/10.1017/S0956796817000120

• Journal Article Type: Article
• Acceptance Date: Aug 22, 2017
• Publication Date: Sep 20, 2017
• Deposit Date: Oct 4, 2017
• Publicly Available Date: Oct 4, 2017
• Journal: Journal of Functional Programming
• Print ISSN: 0956-7968
• Electronic ISSN: 1469-7653
• Publisher: Cambridge University Press
• Peer Reviewed: Peer Reviewed
• Volume: 27
• Article Number: e20
• DOI: https://doi.org/10.1017/S0956796817000120
• Public URL: https://nottingham-repository.worktribe.com/output/883824
• Publisher URL: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/compiling-a-50year-journey/31A66593E940CEF13253C34714F78041
• Related Public URLs: http://www.cs.nott.ac.uk/~pszgmh/fifty.pdf
• Additional Information: This article has been published in a revised form in Journal of Functional Programming http://doi.org/Journal of Functional Programming. This version is free to view and download for private research and study only. Not for re-distribution, re-sale or use in derivative works. © Cambridge University Press 2017
• Contract Date: Oct 4, 2017