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

candle_kernelProgScript.sml: Adds Candle specific functions to the kernel module from ml_hol_kernel_funsProg

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 overloading 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.