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.