@article{fiftyyears,
  Title = {Compiling a 50-year journey},
  Author = {Graham Hutton and Patrick Bahr},
  Year = {2017},
  volume = {27},
  journal = {Journal of Functional Programming},
  Month = sep,
  Date = {2017-09-20},
  DOI = {10.1017/S0956796817000120},
  url = {https://www.cambridge.org/core/journals/journal-of-functional-programming/article/compiling-a-50year-journey/31A66593E940CEF13253C34714F78041},
  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, Rocq, equational reasoning}
}