HOL Light: An Overview

John Harrison.

Proceedings of TPHOLs 2009, the 22nd International Conference on Theorem Proving in Higher Order Logics. Springer LNCS 5674, pp. 60-66.

Abstract:

HOL Light is an interactive proof assistant for classical higher-order logic, intended as a clean and simplified version of Mike Gordon's original HOL system. Theorem provers in this family use a version of ML as both the implementation and interaction language; in HOL Light's case this is Objective CAML (OCaml). Thanks to its adherence to the so-called `LCF approach', the system can be extended with new inference rules without compromising soundness. While retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof tools and has been applied to some non-trivial tasks in the formalization of mathematics and industrial formal verification.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-hollight,
        author          = "John Harrison",
        title           = "{HOL} {L}ight: An Overview",
        editor          = "Stefan Berghofer and Tobias Nipkow and
                           Christian Urban and Makarius Wenzel",
        booktitle       = "Proceedings of the 22nd International Conference on
                           Theorem Proving in Higher Order Logics,
                           TPHOLs 2009",
        address         = "Munich, Germany",
        year            = 2009,
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 5674,
        pages           = "60--66"}