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.