Verification of a HOL theorem prover, based on HOL Light (http://www.cl.cam.ac.uk/~jrh13/hol-light/), implemented in CakeML.

overloading: Definition of the inference system for HOL with ad-hoc overloading, including semantics in set theory and proofs of soundness and consistency.

prover: Proof of soundness for the Candle theorem prover.

set-theory: A specification of (roughly) Zermelo's set theory.

standard: Definition of the inference system for HOL, including semantics in set theory and proofs of soundness and consistency.

syntax-lib: Auxiliary definitions used for manipulating (deeply embedded) HOL syntax.