Compiling a 50-year journey

Graham Hutton; Patrick Bahr

doi:10.1017/S0956796817000120

Compiling a 50-year journey

Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review

Abstract

Fifty years ago, John McCarthy and James Painter 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.

Original language	English
Article number	20
Journal	Journal of Functional Programming
Volume	27
Number of pages	11
ISSN	0956-7968
DOIs	https://doi.org/10.1017/S0956796817000120
Publication status	Published - 20 Sep 2017

Keywords

program calculation
verified compiler
virtual machine
Coq
equational reasoning

Access to Document

10.1017/S0956796817000120

fiftyAccepted author manuscript, 113 KB

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/compiling-a-50year-journey/31A66593E940CEF13253C34714F78041

Cite this

@article{8cab18fe199b482fbf5156386904986e,

title = "Compiling a 50-year journey",

abstract = "Fifty years ago, John McCarthy and James Painter 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.",

keywords = "program calculation, verified compiler, virtual machine, Coq, equational reasoning",

author = "Graham Hutton and Patrick Bahr",

year = "2017",

month = sep,

day = "20",

doi = "10.1017/S0956796817000120",

language = "English",

volume = "27",

journal = "Journal of Functional Programming",

issn = "0956-7968",

publisher = "Cambridge University Press",

}

TY - JOUR

T1 - Compiling a 50-year journey

AU - Hutton, Graham

AU - Bahr, Patrick

PY - 2017/9/20

Y1 - 2017/9/20

N2 - Fifty years ago, John McCarthy and James Painter 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.

AB - Fifty years ago, John McCarthy and James Painter 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.

KW - program calculation

KW - verified compiler

KW - virtual machine

KW - Coq

KW - equational reasoning

U2 - 10.1017/S0956796817000120

DO - 10.1017/S0956796817000120

M3 - Journal article

VL - 27

JO - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

M1 - 20

ER -

Compiling a 50-year journey

Abstract

Keywords

Access to Document

Fingerprint

Cite this