Automated Reasoning Group Old HOL System
This page provides information about various old releases of HOL.
For the latest information see the
current HOL page.
Lab |
ARG |
Description |
HOL |
Isabelle |
Members |
Haiku
The HOL System
The HOL System is an environment for interactive theorem proving in a
higher-order logic. Its most outstanding feature is its high degree of
programmability through the meta-language ML. The system has a wide
variety of uses from formalizing pure mathematics to verification of
industrial hardware. Academic and industrial sites world-wide are using HOL.
The name `HOL' is pronounced either as a word to rhyme with `doll' or letter
by letter. The system is available without charge.
Further Information
How to get the HOL System
The HOL System is currently available in three
versions, HOL98, HOL90, and HOL88. They all implement the same logic,
but offer different functionality.
HOL98 uses
Standard ML
(specifically MoscowML) as both
its implementation language and its meta-language. It features some
important extensions over previous HOL systems. It also runs very well on
small machines. A preliminary user's manual is also available.
HOL90 uses
Standard ML
(specifically Standard ML of New Jersey) as both its implementation language
and its meta-language. It runs well on large machines.
HOL88 is the oldest version, built on top of Lisp. It uses a
non-standard version of ML as its meta-language. Its advantages are that
it may perform better than HOL90 on `small' memory machines (less than
32 Mbytes) and it has better documentation.
HOL98 is available by anonymous ftp from:
HOL88 is available by anonymous ftp from:
HOL90 is available by anonymous ftp from:
Information on building the HOL system for various architectures may be found
by browsing the
archive of the
info-hol mailing list.
User Interfaces for the HOL System
TkHol
TkHol is an
experimental user interface for HOL90 implemented by
Donald Syme using the
Tk/Tcl toolkit.
CHOL
CHOL is a user
interface for HOL built by
Laurent
Théry using the
Centaur system.
It works with both HOL88 and HOL90.
xhol
Tom Schubert and John Biggs
have developed an X interface for HOL88 using the X Toolkit. Their work is
described in a
paper.
The source code can be found
here.
The Emacs Editor
The Emacs
editor can be used as a simple interface to HOL.
Phil Windley
has written a
report on
an Emacs interface for HOL88. For HOL90, the SML-mode for Emacs may be useful.
Documentation for the HOL System
The HOL System comes with a
Tutorial, a
Description, and a
Reference
Manual, plus manuals for each supported library. These are currently oriented
to HOL88 but the Reference Manual is in the
process of being converted to HOL90. There is
also a book based on
the Tutorial and Description (for HOL88):
M. J. C. Gordon and
T. F. Melham (editors),
Introduction to HOL:
A theorem proving environment for higher order logic,
Cambridge University Press, 1993.
A review
of this book by
Graham Hutton
appeared in the Journal of Functional
Programming, 4(4):557-559, October 1994.
Other documentation includes:
Some documentation and other useful information is also available on the Web at
Brigham Young
University, and there is a mailing list for
discussions relating to the HOL system.
Electronic Mail Lists for the HOL System
info-hol
There is an e-mail list for discussions and announcements related to
the HOL System. To join the list send a request to
info-hol-request@lal.cs.byu.edu.
Messages can be sent to the list at
info-hol@lal.cs.byu.edu.
hol2000
Messages relating to the
future development of
the HOL System should be sent to
hol2000@lal.cs.byu.edu.
To subscribe to this list, send a request to
hol2000-request@lal.cs.byu.edu. A
list of subscribers is available.
Searching the mailing lists
You can search the info-hol and hol2000 mailing lists (as well as the
HOL Reference Manual) by
clicking here
and selecting the appropriate item in the search menu.
Applications of the HOL System
Hardware Verification
Software Verification
Users of the HOL System
The HOL System is used at academic and industrial
sites in many countries.
A summary
has been created by
Sara Kalvala. A list of Web
sites follows:
- Åbo Akademi
-
Programming Methods Group,
Department of Computer Science,
Åbo Akademi University,
Finland
- Bell Laboratories
- Bell Laboratories, USA
- Brigham Young
-
Laboratory for Applied Logic,
Brigham Young University, USA
- Cambridge
-
Automated Reasoning Group,
University of Cambridge Computer
Laboratory, UK
- Glasgow
-
Formal Methods Group,
Department of Computing Science,
University of Glasgow, UK
- Karlsruhe
-
Hardware Verification Group,
Institute of Computer
Design and Fault Tolerance,
Department
of Computer Science,
University of Karlsruhe, Germany
Conferences Related to the HOL System
There has been a series of international conferences on
the HOL System. The first three were informal users'
meetings with no published proceedings. The tradition now is for an annual
conference in a continent different to the location of the previous meeting.
From 1996 the scope broadened to cover all theorem proving in higher-order
logics.
TPHOLs Conferences
- 2003
- The 16th International
Conference on Theorem Proving in Higher Order Logics,
Rome, Italy,
9-12 September 2003.
- 2002
- The 15th International
Conference on Theorem Proving in Higher Order Logics,
Hampton, Virginia, USA,
20-23 August 2002.
- 2001
- The 14th International
Conference on Theorem Proving in Higher Order Logics,
Edinburgh, Scotland,
3-6 September 2001.
BibTeX file /
Proceedings.
- 2000
- The 13th International
Conference on Theorem Proving in Higher Order Logics,
DoubleTree Hotel, Portland, Oregon, USA,
14-18 August 2000.
BibTeX file /
Proceedings.
- 1999
- The 12th International
Conference on Theorem Proving in Higher Order Logics,
Unversity of Nice-Sophia-Antipolis,
Nice, France,
14-17 September 1999.
BibTeX file.
- 1998
- The 11th International Conference
on Theorem Proving in Higher Order Logics,
The Australian National University,
Canberra,
Australia, 28 September - 1 October 1998.
BibTeX file.
- 1997
- The 10th
International Conference on Theorem Proving in Higher Order Logics,
Bell Labs,
Murray Hill,
New Jersey, USA, 19-22 August 1997.
BibTeX file.
- 1996
- The 9th International
Conference on Theorem Proving in Higher Order Logics,
Turku Center for Computer Science
(TUCS) and
Åbo Akademi University,
Turku,
Finland
(map),
26-30 August 1996.
BibTeX file.
HOL Workshops
- 1995
- 8th International
Workshop on Higher Order Logic Theorem Proving and its Applications,
Aspen Grove, Utah, USA,
11-14 September 1995.
BibTeX file.
- 1994
- 7th International Workshop
on Higher Order Logic Theorem Proving and its Applications, Valletta,
Malta,
19-22 September 1994.
BibTeX file /
Photograph
(1MB).
- 1993
- 6th International Workshop on Higher Order Logic Theorem Proving and its
Applications, Vancouver, B.C., Canada, 10-13 August 1993.
BibTeX file /
Photograph
(2.6MB).
- 1992
- 5th International
Workshop on Higher Order Logic Theorem Proving and its Applications,
IMEC, Leuven, Belgium, 21-24 September 1992.
BibTeX file /
Photograph
(1.3MB).
- 1991
- 4th International Workshop on the HOL Theorem Proving System and its
Applications, Davis, California, USA, 28-30 August 1991.
BibTeX file.
HOL Users Meetings
- 1990
- 3rd International HOL Users Meeting, Aarhus University, Denmark,
1-2 October 1990.
Copies of the overhead transparencies from the talks were published as a
technical report (BibTeX file).
Abstracts (DVI) /
Abstracts (PostScript) /
Photograph
(1.3MB).
- 1989
- 2nd International HOL Users Meeting, Trinity Hall, Cambridge,
14-15 December 1989.
Abstracts (DVI) /
Abstracts (PostScript) /
Photograph
(4.3MB).
- 1988
- 1st International HOL Users Meeting, Sidney Sussex College, Cambridge,
29-30 September 1988.
Photograph
(2.5MB).
Other Conferences
- FMCAD'96
- The International Conference on Formal Methods in Computer-Aided Design,
Palo Alto, CA, USA, 6-8 November 1996.
- DCC'96
- The Third Workshop on Designing Correct Circuits, Båstad, Sweden,
2-4 September 1996.
- TPCD'94
- 2nd International Conference on Theorem Provers in Circuit Design:
Theory, Practice and Experience, Bad Herrenalb (Blackforest), Germany,
26-28 September 1994.
- TPCD'92
- International Conference on Theorem Provers in Circuit Design:
Theory, Practice and Experience, Nijmegen, The Netherlands,
22-24 June 1992.
Special Journal Issues on the HOL System
There have been a number of journal issues devoted to research related to
the HOL System and higher-order logic theorem proving in
general.
- Formal Methods in System Design, Volume 3, Numbers 1/2.
- Kluwer Academic Publishers, August 1993.
Special Issue on Higher Order Logic Theorem Proving and its Applications, I.
Guest Editors: Luc Claesen and
Michael Gordon.
BibTeX file.
- Formal Methods in System Design, Volume 5, Numbers 1/2.
- Kluwer Academic Publishers, July 1994.
Special Issue on Higher Order Logic Theorem Proving and its Applications, II.
Guest Editors: Luc Claesen and
Michael Gordon.
BibTeX file.
- The Computer Journal,
Volume 38, Number 2.
- The British Computer Society/Oxford University Press, 1995.
Special Issue on Higher Order Logic Theorem Proving and its Applications.
Guest Editor:
T. F. Melham.
BibTeX file.
History of the HOL System
(Based on the preface to the HOL system
Description.)
The HOL System is designed to support interactive
theorem proving in higher order logic (hence the acronym `HOL'). To this end,
the formal logic is interfaced to a general purpose programming language (ML,
for meta-language) in which terms and theorems of the logic can be denoted,
proof strategies expressed and applied, and logical theories developed.
The version of higher order logic used in HOL is predicate calculus with terms
from the typed lambda calculus (i.e. simple type theory). This was originally
developed as a foundation for mathematics [1]. The
primary application area of HOL was initially intended to be the specification
and verification of hardware designs. (The use of higher order logic for this
purpose was first advocated by
Keith
Hanna [3].) However, the logic does not restrict
applications to hardware; HOL has been applied to many other areas.
The approach to mechanizing formal proof used in HOL is due to Robin Milner
[2], who also headed the team that designed and
implemented the language ML. That work centred on a system called LCF (logic
for computable functions), which was intended for interactive automated
reasoning about higher order recursively defined functions. The interface of
the logic to the meta-language was made explicit, using the type structure of
ML, with the intention that other logics eventually be tried in place of the
original logic. The HOL system is a direct descendant of LCF; this is
reflected in everything from its structure and outlook to its incorporation of
ML, and even to parts of its implementation. Thus HOL satisfies the early plan
to apply the LCF methodology to other logics.
The original LCF was implemented at Edinburgh in the early 1970's, and is now
referred to as `Edinburgh LCF'. Its code was ported from Stanford Lisp to
Franz Lisp by Gérard Huet at
INRIA, and was used in a
French research project called
`Formel'. Huet's Franz
Lisp version of LCF was further developed at Cambridge by
Larry Paulson, and became
known as `Cambridge LCF'. The HOL system is implemented on top of an early
version of Cambridge LCF and consequently many features of both Edinburgh and
Cambridge LCF were inherited by HOL. For example, the axiomatization of higher
order logic used is not the classical one due to Church, but an equivalent
formulation influenced by LCF.
The language ML has now achieved status as a programming language in its own
right, although it was originally designed as the proof management language
for LCF. It is a functional language distinguished particularly for its type
inference mechanism, that gives type security without overburdening the user.
Types, and especially abstract types, are the basis for distinguishing the
theorems of a logic from arbitrary formulae, in a secure way. A standard has
now been established for ML [4]. The most recent
version of Cambridge LCF, which is documented in Paulson's book
[5], is based on this
Standard ML.
The original HOL system included an earlier version of ML, as did the enhanced
and rationalized version, called HOL88, which
was released (in 1988) after the original HOL system had been in use for
several years. In the early 1990's HOL90, an
implementation of HOL based on Standard ML rather than Lisp, was developed by
Konrad Slind, initially at the
University of Calgary. A commercial version of HOL using Standard ML was also
developed by ICL Secure Systems. This system, now called ProofPower, is a
`highly assured' system for commercial verification projects in the safety and
security critical areas.
A proposal has
been put forward to develop a new version of HOL around the year 2000 that
will incorporate some of the results of research into the HOL system and its
applications, and other theorem proving technology. There is an
electronic mailing list for discussion of this
subject.
- A. Church,
"A Formulation of the Simple Theory of Types",
Journal of Symbolic Logic Vol. 5 (1940), pp. 56-68.
- M. Gordon, R. Milner and
C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation,
Lecture Notes in Computer Science, Vol. 78, Springer-Verlag, 1979.
- F. K.
Hanna and N. Daeche,
"Specification and Verification Using Higher-Order Logic: A Case Study".
In Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh
Workshop on VLSI, edited by G. Milne and P. A. Subrahmanyam,
North-Holland, 1986, pp. 179-213.
- R. Milner, M. Tofte and R. Harper, The Definition of Standard ML,
The MIT Press, 1990.
- L. Paulson,
Logic and Computation: Interactive Proof with Cambridge LCF,
Cambridge Tracts in Theoretical Computer Science 2,
Cambridge University Press, 1987.
Systems Related to HOL
There are a number of theorem proving systems related to
the HOL System; some of them are listed below.
Carolyn Talcott and
Michael
Kohlhase have put together a page on mechanized reasoning. The page is
mirrored in the
USA and
Germany.
- ACL2
- ACL2 is a theorem proving system produced at Computational Logic, Inc.
The acronym ``ACL2'' stands for ``A Computational Logic for Applicative Common
Lisp.'' ACL2 is similar to the Boyer-Moore theorem prover,
Nqthm, and
Kaufmann's interactive extension, Pc-Nqthm. However, instead of supporting
the ``Boyer-Moore logic,'' ACL2 supports a large applicative subset of Common
Lisp. Furthermore, ACL2 is programmed almost entirely within that language.
- CLAM
- CLAM is a proof planner from the
Mathematical Reasoning Group
at the Department of Artificial Intelligence, University of Edinburgh.
- Coq
- The Coq proof assistant allows mechanical manipulation of assertions of
the "Calculus of Inductive Constructions", interactive development of formal
proofs, and synthesis of certified programs from the constructive proofs of
their specifications.
- Eves
- Eves is a verification environment, the main component of which is a
theorem prover called Never.
- Gypsy
- Gypsy is a verification environment with its own language.
- Isabelle
- Isabelle is a generic theorem prover written in
Standard ML. It is
generic in the sense that users can define their own logic using a metalogic.
Isabelle has a number of things in common with HOL: a programming
meta-language, tactics and tacticals, and a fully-expanded proof is generated
(over time). There are also significant differences, e.g., rules are not
implemented as ML functions but are represented as explicit structures, and
higher-order resolution is used for proof construction.
- LAMBDA
- LAMBDA is a commercial system similar to Isabelle but specialised to a
classical higher-order logic with polymorphism like the one mechanised in the
HOL system. Early versions implemented a constructive logic of partial terms.
The system comes with a graphical interface for hardware design called DIALOG.
- LP
- The Larch Prover is an interactive theorem proving system for multisorted
first-order logic.
- Nqthm
(The Boyer-Moore Theorem Prover)
- Nqthm is a theorem proving system for a computational logic. The
logic is (intentionally) similar to the core of the Lisp programming language.
It is untyped, quantifier free, and first order. Nqthm provides a high degree
of automation in terms of heuristics for simplification, induction, and
related activities. A proof in the system is generated by making definitions
and then calling the heuristics on the conjecture to be proved. The proof
attempt will typically fail, but examination of the prover's log (which is in
English) will reveal either a flaw in the conjecture or a lemma that the
prover needs to be aware of to succeed. The user then asks the system to prove
this lemma (possibly requiring other lemmas to be proved) and repeats the
attempt to prove the original conjecture. This process continues until the
prover succeeds on the conjecture.
- Nuprl
- Nuprl is another system descended from LCF. Its
logic is based on Martin-Löf's intuitionistic (constructive) type theory.
The infrastructure of Nuprl has much in common with HOL, but differs in that
proofs are represented explicitly as objects. However, these are not full
proofs in terms of primitive inferences; each node of the proof
tree corresponds to the application of a tactic which might be at a high
level. Nevertheless, this helps users to examine the proof, and facilitates
backtracking and alternative proof attempts.
- OBJ
- OBJ is based on order-sorted equational logic and is organised in
parameterised modules.
- ProofPower
- ProofPower is a commercial implementation of HOL by ICL Secure Systems. It
is being used for formal reasoning about Z specifications.
- PVS
- The Prototype Verification System from SRI International is an interactive
system for a higher order logic with dependent types. It has its own
specification language. Significant automation is achieved using decision
procedures for various theories including linear arithmetic.
- RRL
- Rewrite Rule Laboratory is a theorem prover for first-order logic with an
emphasis on equational reasoning.
- SDVS
- The State Delta Verification System is a verification system that
incorporates simplifiers, decision procedures and symbolic execution. It is
based on a temporal logic and has been mainly used for verification of
computer descriptions written in languages such as Ada and VHDL.
- Veritas
- Veritas is a logic developed by
Keith
Hanna to support formal design methods. It is motivated by
Martin-Löf's intuitionistic (constructive) type theory: it is higher
order and provides dependent types and subtypes, but it is a classical rather
than a constructive logic. The Veritas-90 version is implemented in both
Standard ML and
Haskell.
The intention behind the implementation in the purely-functional language
Haskell is to enable parallel evaluation. As in HOL, abstract data types are
used to securely implement the various syntactic categories of the logic, but
in addition to terms and theorems being implemented in this way, so is the
representation of theories, which are first-class objects in Veritas. In HOL,
theories are structures that are modified imperatively. In Veritas, a
purely-functional view is taken.
Lab |
ARG |
Description |
HOL |
Isabelle |
Members |
Haiku
Page last updated on Tue Oct 10 17:56:25 BST 2000
by Daryl (djs1002@cl.cam.ac.uk)