An SCPOG checker built on CakeML with arrays.
proofs: Prove end-to-end correctness theorem for SCPOG checker with arrays.
scpogCompileScript.sml: Compiles the scpog example by evaluation inside the logic of HOL
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||
An SCPOG checker built on CakeML with arrays.
proofs: Prove end-to-end correctness theorem for SCPOG checker with arrays.
scpogCompileScript.sml: Compiles the scpog example by evaluation inside the logic of HOL