Definition of the inference system for HOL with ad-hoc overloading, including semantics in set theory and proofs of soundness and consistency.
ml_checker: Implementation of an I/O shim for extracting a cyclicity checker binary.
ml_kernel: Implementation of the monadic functions in (deeply embedded) CakeML, generated by the translator (proof-producing synthesis).
monadic: Implementation of the Candle kernel as monadic functions in HOL (i.e. a shallow embedding), and proof that they refine the HOL inference system.
semantics: Semantics, soundness, and consistency for the HOL inference system with ad-hoc overloading of constant definitions.
syntax: Syntax of the HOL inference system with ad-hoc overloading.