The HOL theorem prover

Please mail J.P.Bowen@reading.ac.uk if you know of relevant on-line information not included here.

This document contains some pointers to information on the HOL mechanical theorem proving system, based on Higher Order Logic, available around the world on the World Wide Web (WWW or W3), a global hypermedia system providing worldwide information.

TPHOLs'98: International Conference on Theorem Proving in Higher Order Logics, Canberra, Australia, 21 September - 2 October 1998.

The following on-line information is available:

The HOL System. Information provided by the Automated Reasoning Group at the University of Cambridge Computer Laboratory, UK. See also FTP archive.
HOL documentation at Brigham Young University (second sourced in the UK).
The sources for the HOL system (with an index) at the University of Cambridge Computer Laboratory (second sourced in the US).
Archive material including papers and contributed software for HOL (with a README file) are available.
Release Note for HOL from the Automated Reasoning Group at Cambridge.
The info-hol electronic mailing list enables discussion on topics concerning HOL and includes annnouncements of HOL meetings. Contact info-hol-request@lal.cs.byu.edu to be added to the list. The archives are searchable and there is a list of subscribers.
Conferences related to the HOL System. See TPHOLs'98: International Conference on Theorem Proving in Higher Order Logics, Canberra, Australia, 21 September - 2 October 1998.
The HOL2000 initiative is trying to put together a design for the next generation of HOL-like theorem proving environments. To join the discussion list, email hol2000-request@lal.cs.byu.edu.
Some support for the Z notation is available as documented in the paper Z and HOL. The source files for various Z specifications in HOL are available.
ProofPower is a commercial tool, developed and marketed by ICL, supporting development and checking of specifications and formal proofs in Higher Order Logic and/or Z. Support for Z uses a deep(ish) embedding of Z into HOL, but includes syntax and type checking customized for Z. Contact ProofPower-server@win.icl.co.uk for further information.
HOL-Z tool. A shallow embedding of the Z notation in the higher-order logic theorem prover Isabelle, similar to that of the HOL system. Also mirrored here and here.
Information on the HOL Theorem Prover from the Formal Methods and Theory Group at Glasgow.
A good introductory book is Introduction to HOL: A theorem proving environment for higher order logic, edited by M.J.C. Gordon and T.F. Melham, 1993. ISBN: 0 521 44189 7 See also:
- Other information on books, especially concerning hardware verification.
- Publishers information from ' Cambridge University Press. ISBN: 0 521 44189 7.
- A book review of ``An introduction to HOL'' by Graham Hutton.
- Order from your bookstore (e.g., Blackwell's (UK) from here or Amazon.com Books (USA) from here).
A five day HOL training course is available from the University of Glasgow, Scotland.
Information on HOL and other automated reasoning systems in a standard format is available from Stanford University.
Higher Order Logic theorem provers pointers from Yahoo.
CHOL distribution from INRIA, an attempt to privide a better user interface for HOL using the Centaur system.
Higher Order Logic Theorem Proving and its Applications special issue of The Computer Journal by Tom Melham.
Tools supporting HOL listed in the FME Tools Database.
HOL Light by John Harrison.

See also PVS, another newer theorem proving tool based on higher order logic.

Last updated by Jonathan Bowen, 7 July 1999.
Further information for possible inclusion is welcome.

Part of the OUCL archive.