HOL with Definitions: Semantics, Soundness, and a Verified Implementation

Abstract. We present a mechanised semantics and soundness proof for the HOL Light kernel including its definitional principles, extending Har-rison’s verification of the kernel without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Our semantics is the first for Wiedijk’s stateless HOL; our implementation, however, is stateful: we give semantics to the stateful inference system by translation to the stateless. We improve on Harri-son’s approach by making our model of HOL parametric on the universe of sets. Finally, we prove soundness for an improved principle of con-stant specification, in the hope of encouraging its adoption. This paper represents the logical kernel aspect of our work on verified HOL imple-mentations; the production of a verified machine-code implementation of the whole system with the kernel as a module will appear separately.