HOL Light: A Tutorial Introduction

John Harrison.

Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Springer LNCS 1166, pp. 265-269, 1996.

Abstract:

HOL Light is a new version of the HOL theorem prover. While retaining the reliability and programmability of earlier versions, it is more elegant, lightweight, powerful and automatic; it will be the basis for the Cambridge component of the HOL-2000 initiative to develop the next generation of HOL theorem provers. HOL Light is written in CAML Light, and so will run well even on small machines, e.g. PCs and Macintoshes with a few megabytes of RAM. This is in stark contrast to the resource-hungry systems which are the norm in this field, other versions of HOL included. Among the new features of this version are a powerful simplifier, effective first order automation, simple higher-order matching and very general support for inductive and recursive definitions.

Many theorem provers, model checkers and other hardware verification tools are tied to a particular set of facilities and a particular style of interaction. However HOL Light offers a wide range of proof tools and proof styles to suit the needs of various applications. For work in high-level mathematical theories, one can use a more `declarative' textbook-like style of proof (inspired by Trybulec's Mizar system). For larger but more routine and mechanical applications, HOL Light includes more `procedural' automated tools for simplifying complicated expressions, proving large tautologies etc. We believe this unusual range makes HOL Light a particularly promising vehicle for floating point verification, which involves a mix of abstract mathematics and concrete low-level reasoning. We will aim to give a brief tutorial introduction to the system, illustrating some of its features by way of such floating point verification examples. In this paper we explain the system and its possible applications in a little more detail.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-demo,
        title           = "{HOL} Light: A Tutorial Introduction",
        author          = "John Harrison",
        booktitle       = "Proceedings of the First International Conference on
                           Formal Methods in Computer-Aided Design
                           ({FMCAD}'96)",
        editor          = "Mandayam Srivas and Albert Camilleri",
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 1166,
        year            = 1996,
        pages           = "265--269"}