Compiling a 50-year journey*. (20th September 2017)

• Record Type: Journal Article
• Authors: HUTTON, GRAHAM; BAHR, PATRICK
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2017-09-20
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796817000120
• Languages: English
• ISSNs: 0956-7968

Abstract

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.