Automated Reasoning Group Old HOL System

University of Cambridge Computer Laboratory 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.

References

  1. A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic Vol. 5 (1940), pp. 56-68.
  2. 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.
  3. 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.
  4. R. Milner, M. Tofte and R. Harper, The Definition of Standard ML, The MIT Press, 1990.
  5. 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)