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.

@article{HuttonB17,
  title = {Compiling a 50-year journey},
  author = {GRAHAM HUTTON and PATRICK BAHR},
  journal = {Journal of Functional Programming},
  volume = {27},
  year = {2017},
  doi = {10.1017/s0956796817000120}
}