feat(archive): formalize compiler correctness by McCarthy and Painter… · leanprover-community/mathlib@df45002 · GitHub

Commit

feat(archive): formalize compiler correctness by McCarthy and Painter (…

Browse files

…#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.

Loading branch information

xiw committed Oct 21, 2020

1 parent 1b4e769 commit df45002