Towards self-verification of HOL Light

John Harrison.

Proceedings of IJCAR 2006, the third International Joint Conference on Automated Reasoning. Springer LNCS 4130, pp. 177-191.

Abstract:

The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional OCaml, whose complete formal verification seems to be quite feasible. We would like to formally verify (i) that the abstract HOL logic is indeed correct, and (ii) that the OCaml code does correctly implement this logic. We have performed a full verification of an imperfect but quite detailed model of the basic HOL Light core, without definitional mechanisms, and this verification is entirely conducted with respect to a set-theoretic semantics within HOL Light itself. We will duly explain why the obvious logical and pragmatic difficulties do not vitiate this approach, even though it looks impossible or useless at first sight. Extension to include definitional mechanisms seems straightforward enough, and the results so far allay most of our practical worries.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-holhol,
        author          = "John Harrison",
        title           = "Towards self-verification of HOL Light",
        editor          = "Ulrich Furbach and Natarajan Shankar",
        booktitle       = "Proceedings of the third International Joint 
                           Conference, IJCAR 2006",
        address         = "Seattle, WA",
        year            = 2006,
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 4130,
        pages           = "177--191"}