Compiling a 50-year journey

Graham Hutton, Patrick Bahr

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-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 languageEnglish
Article number20
JournalJournal of Functional Programming
Volume27
Number of pages11
ISSN0956-7968
DOIs
Publication statusPublished - 20 Sep 2017

Keywords

  • program calculation
  • verified compiler
  • virtual machine
  • Coq
  • equational reasoning

Fingerprint

Dive into the research topics of 'Compiling a 50-year journey'. Together they form a unique fingerprint.

Cite this