A Verified Theorem Prover for Higher-Order Logic

Sammanfattning: This thesis is about mechanically establishing the correctness of computer programs. In particular, we are interested in establishing the correctness of tools used in computer-aided mathematics. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. With these, we have produced an interactive theorem prover for higher-order logic, called Candle, that is verified to accept only true theorems. To the best of our knowledge, Candle is the only interactive theorem prover for higher-order logic that has been verified to this degree. Candle and all technology that underpins it is developed using the HOL4 theorem prover. We use proof-producing synthesis and the verified CakeML compiler to obtain a machine code executable for the Candle theorem prover. Because the CakeML compiler is verified to preserve program semantics, we are able to obtain a soundness result about the machine code which implements the Candle theorem prover.