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.

## 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"}