Skip to content

Latest commit

 

History

History
5 lines (4 loc) · 222 Bytes

README.md

File metadata and controls

5 lines (4 loc) · 222 Bytes

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.