Skip to content

Latest commit

 

History

History
32 lines (24 loc) · 1.31 KB

README.md

File metadata and controls

32 lines (24 loc) · 1.31 KB

Implementation of the monadic functions in (deeply embedded) CakeML, generated by the translator (proof-producing synthesis).

lisp: Parsing and pretty printing of simple s-expressions

ml_hol_initScript.sml: Prove that the state of the kernel can be initialised in a way that meets the invariants (STATE and HOL_STORE).

ml_hol_kernelProgScript.sml: Close the kernel module from ml_hol_kernel_funsProg

ml_hol_kernel_funsProgScript.sml: Apply the monadic translator to the Candle kernel to generate the deeply embedded CakeML code for the kernel. As a side effect, the monadic translator proves certificate theorems that state a formal connection between the generated code and the input HOL functions.

ppKernelScript.sml: Pretty prints the CakeML code of the Candle kernel. The output is produced in a file called kernel_ml.txt.

print_thmScript.sml: Defines functions for turning a ctxt & thm to a string and back

runtime_checkLib.sml: Mechanism for adding runtime type checking annotations, used in the Candle prover soundness proofs.

runtime_checkScript.sml: Theorems and definitions to support adding runtime type checking annotations.