Compiling a 50-year journey
Journal of Functional Programming, 27, 2017.
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.
Categories: Compilers, Formal Verification
Tags: Program Calculation, Verified Compiler, Virtual Machine, Coq, Equational Reasoning