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.

Categories: Compilers, Formal Verification

Tags: Program Calculation, Verified Compiler, Virtual Machine, Coq, Equational Reasoning