Correctness of a compiler for arithmetic expressions in Lean

“Correctness of a compiler for arithmetic expressions” (McCarthy and Painter 1967) describes the first proof of compiler correctness. To make it easier to play with the proof, I coded it up using the Lean theorem prover.

The Lean code is self-explanatory, so I won’t go into the details here.

Browse the Lean code on GitHub.
Run in the browser (laptop or desktop recommended; tested with Lean/mathlib 3.21.0c).

Lean’s support for calculational proofs is particularly nice for mirroring the proof in the paper. For example, below is an excerpt of the proof in the paper:

\[\begin{aligned} \zeta_1 & = \mathit{outcome}(\mathit{compile}(s1(e),t),\eta) \\ & =_t a(\mathit{ac}, \upsilon_1, \eta) & \textrm{Induction Hypothesis} \end{aligned}\]

Here’s the corresponding part in Lean:

calc ζ₁
    = outcome (compile map e_s₁ t) η : by cc
... ≃[t] {ac := ν₁, ..η}             : by apply e_ih_s₁; assumption

Typos

The reprint version of the paper contains a number of typos (not present in the original version):

Theorem 1: “\(c(\mathit{loc}(v, \eta) = c(v, \xi)\)” should be “\(c(\mathit{loc}(v, \mathit{map}), \eta) = c(v, \xi)\).”
Section 5.III, under “\(\zeta_2 = \mathit{outcome}(\mathit{mksto}(t), \zeta_1)\)”: “\(a(t, \upsilon_1), \zeta_1)\)” should be “\(a(t, \upsilon_1, \zeta_1)\).”
Section 5.III, next to “\(c(\mathit{loc}(\upsilon, \mathit{map}), \zeta_2)\)”: “\(c(\mathit{loc}(\upsilon), \mathit{map})a(t, \upsilon_1, \eta))\)” should be “\(c(\mathit{loc}(\upsilon, \mathit{map}), a(t, \upsilon_1, \eta))\).”

Typos

Links