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