Correctness proof for the CakeML compiler.
compilerProofScript.sml: Prove top-level correctness theorem for complete compiler, i.e. the combination of parsing, type inference, compiler backend.
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||
Correctness proof for the CakeML compiler.
compilerProofScript.sml: Prove top-level correctness theorem for complete compiler, i.e. the combination of parsing, type inference, compiler backend.