Repository logo
 

Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation


Change log

Authors

Kumar, R 
Arthan, R 
Myreen, MO 
Owens, S 

Abstract

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison’s verification of the inference system 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. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison’s work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk’s Stateless HOL.

Description

This is the final version of the article. It first appeared from Springer via http://dx.doi.org/10.1007/s10817-015-9357-x

Keywords

HOL, Higher-order logic, Verification, Interactive theorem proving, Theorem proving, Consistency, Semantics, Self-formalisation, Self-verification

Journal Title

Journal of Automated Reasoning

Conference Name

Journal ISSN

0168-7433
1573-0670

Volume Title

56

Publisher

Springer Science and Business Media LLC
Sponsorship
The first author was supported by the Gates Cambridge Trust. The second author was funded in part by the EPSRC (grant number EP/K503769/1). The third author was partially supported by the Royal Society UK and the Swedish Research Council.