NetNews Usenet Archive 1992 #30/NN_1992_30.iso/spool/comp/archives/3792

Internet Message Format | 1992-12-16 | 5.7 KB

Path: sparky!uunet!spool.mu.edu!agate!agate!usenet
From: [e-mail] (John Harrison)
Newsgroups: comp.archives
Subject: [comp.specification] Release of HOL version 2.01
Followup-To: comp.specification,comp.theory,sci.logic
Date: 16 Dec 1992 09:27:56 GMT
Organization: Cambridge Hardware Verification Group
Lines: 140
Sender: adam@soda
Approved: adam@soda
Distribution: world
Message-ID: <[e-mail]>
References: <[e-mail]>
Reply-To: [e-mail]
NNTP-Posting-Host: soda.berkeley.edu
X-Original-Newsgroups: comp.specification,comp.theory,sci.logic
X-Original-Date: 8 Dec 92 11:03:08 GMT

Archive-name: auto/comp.specification/Release-of-HOL-version-2-01


                 HOL-88 Version 2.01 ("Classic HOL")

This is to announce the release of Version 2.01 of the interactive theorem
prover HOL. The release includes a few minor changes and bugfixes and several
new libraries, including a derived proof procedure for linear arithmetic and a
definitional theory of real numbers.

* WHAT IS HOL?

HOL (Higher Order Logic) is an interactive computer theorem-prover descended
from LCF. The two main references for LCF are:

 o M. J. C. Gordon, R. Milner, C. P. Wadsworth
   Edinburgh LCF: A mechanised logic of computation.
   Springer Lecture Notes in Computer Science #78.
   Springer-Verlag 1979.

 o L. C. Paulson
   Logic and Computation: Interactive proof with Cambridge LCF.
   Cambridge Tracts in Theoretical Computer Science #2.
   Cambridge University Press 1987.

Distinguishing features of HOL are:

 o It uses ML (meta-language), a high-level (impure) functional programming
   language featuring strong polymorphic typing: this allows the user to
   program custom proof procedures.

 o It encapsulates theorems as an ML abstract type whose only constructors
   are the small number of primitive inference rules. This gives a high degree
   of security since the critical core is small, and it is not necessary to be
   a logician to securely extend the reasoning tools available.

 o All theories are built up by conservative, definitional extension,
   which again gives security (no extra axioms are asserted).

 o Additional tools provide backward (goal-directed) theorem proving which can
   be freely mixed with forward proof.

The HOL logic is a descendent of Church's Simple Theory of Types with the
addition of object language polymorphism a la Milner.

* WHERE IS HOL USED, AND WHAT FOR?

HOL was designed mainly for the verification of hardware, but is now used at
many companies, government organizations and higher education institutions
worldwide for hardware, software and protocol verification as well as proof
checking pure mathematics.

There is a HOL users' mailing list; to join send mail to

  [e-mail]

There is also an annual international meeting; the proceedings of the 1991
meeting are available as:

 o Proceedings of the 1991 International Workshop on the HOL theorem proving
   system and its applications, Davis, California.
   Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (eds.)
   IEEE Computer Society Press 1992
   ISBN 0-8186-2460-4 (paper)

The proceedings of the 1992 meeting will be published in the near future.

* HOW DO I LEARN TO USE HOL?

HOL is conceptually a simple system, but the proof tools available are numerous
and sometimes hard to understand. In consequence it can present many
difficulties for a beginner. Training courses are organized periodically: these will
normally be advertised on the "info-hol" mailing list (see above).

The HOL release contains machine-readable (LaTeX etc.) versions of the four
HOL system manuals: Reference, Description, Libraries and Tutorial.

A book on HOL will be available in early 1993:

 o Introduction to HOL
   M. J. C. Gordon & T. F. Melham (eds.)
   Cambridge University Press 1993
   ISBN 0-521-441897

* HOW DO I GET HOL RUNNING?

HOL works on most modern machines given a suitable LISP, in particular Sun
workstations, DEC Mips machines, and PCs and Apple Macintoshes (with at least 8Mbytes
of RAM).

HOL is available free of charge. The most straightforward way of obtaining it
is by FTP, from either of the following two sites:

  ftp.cl.cam.ac.uk [128.232.0.56] in directory "hvg/hol"

  ted.cs.uidaho.edu [129.101.100.20] in directory "pub/hol"

The two main files are "holsys.tar.Z" and "holdoc.tar.Z", which are
compressed tarfiles of, respectively, the hol system (i.e. code, theories)
and the hol documentation (help files and stuff to build the manuals).
There are other odds and ends available too, mostly concerned with
particular LISPs.

HOL can also be supplied on magnetic tape for the benefit of users without FTP
access; contact "[e-mail]" for more details.

* OTHER VERSIONS OF HOL

An alternative to the Cambridge version of HOL is HOL-90, which has a similar
proof system, but is based on a more recent version of ML, Standard ML. It is
in many ways more regular but does not yet support all the Cambridge HOL
libraries. For more details, contact Konrad Slind
([e-mail]). It may be obtained from:

  fsa.cpsc.ucalgary.ca [136.159.2.1] in directory "pub"

A commercial theorem-proving system, based on HOL, but not close to it in
detail, is ICL ProofPower. It is intended for high integrity applications.
For more details contact Roger Jones ([e-mail]).

Queries or requests for more details should preferably be sent by email to

  [e-mail]

or may alternatively be sent to me personally.

Regards,

  John Harrison ([e-mail])

  Hardware Verification Group
  University of Cambridge Computer Laboratory
  New Museums Site
  Pembroke Street
  Cambridge CB2 3QG
  England.

  Phone: [phone]
  Fax:   [phone]