Definition of the inference system for HOL, including semantics in set theory and proofs of soundness and consistency.
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.
opentheory: Implementation of an OpenTheory reader based on the Candle kernel.
semantics: Semantics, soundness, and consistency for the HOL inference system.
syntax: Syntax of the HOL inference system.