Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-21 15:31 df450024

View on Github →

feat(archive): formalize compiler correctness by McCarthy and Painter (#4702) Add a formalization of the correctness of a compiler from arithmetic expressions to machine language described by McCarthy and Painter, which is considered the first proof of compiler correctness.

Estimated changes

added def arithcc.compile
added inductive arithcc.expr
added inductive arithcc.instruction
added def arithcc.loc
added def arithcc.outcome
added theorem arithcc.outcome_append
added def arithcc.read
added def arithcc.register
added structure arithcc.state
added def arithcc.state_eq
added def arithcc.step
added def arithcc.value
added def arithcc.word
added def arithcc.write