Skip to main content

Research Repository

See what's under the surface

Advanced Search

Compiling a 50-year journey

Hutton, Graham; Bahr, Patrick

Authors

Patrick Bahr paba@itu.dk



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.

Journal Article Type Article
Publication Date Sep 20, 2017
Journal Journal of Functional Programming
Print ISSN 0956-7968
Electronic ISSN 1469-7653
Publisher Cambridge University Press (CUP)
Peer Reviewed Peer Reviewed
Volume 27
Article Number e20
APA6 Citation Hutton, G., & Bahr, P. (2017). Compiling a 50-year journey. Journal of Functional Programming, 27,
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
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.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

Files

fifty.pdf (115 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

;