A formalization of "Correctness of a compiler for arithmetic expressions" (McCarthy and Painter 1967) using the Lean theorem prover.
The code has been merged into mathlib. Please visit mathlib for the latest version.
This repository was archived by the owner on Oct 22, 2020. It is now read-only.
xiw/arithcc
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|