ANU: The Australian National University
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [COMP8033] [ML] [HOL] [Exercises] [Lectures] [Assignments]
_____________________________________________________________________

HOL: The Higher Order Logic Theorem Prover

What is HOL?

HOL is one of a family of theorem provers that share a common design called the `LCF architecture'. The LCF architecture is so named because its first use was in a theorem prover called LCF. Users of LCF architecture tools prove theorems in the logic supported by the tool (the object language) by writing programs to construct a proof using a programming language (the meta-language). The object language of the HOL system is a classical higher-order logic based on Church's simple theory of types. The meta-language, as with other LCF provers, is ML.

The original motivation for building HOL was as a tool for assisting in the specification and verification of digital hardware, the higher-order logic supported by HOL is particularly well suited to such problems. However, the logic is a general one, and HOL has now been applied to many different kinds of problems.

Which Particular HOL?

There are three main versions of HOL: HOL88, HOL90 and HOL98. Each of these versions is implemented using a different dialect of ML. HOL88 uses Classic ML, HOL90 uses New Jersey Standard ML, and HOL98 uses Moscow ML. We will be using HOL98 on this course.

The differences between the various versions of the HOL system are not great, which is good, because much of the documentation hasn't been updated since HOL88! The most obvious differences between HOL88 and HOL98 are really the differences between Classic ML and Standard ML (Moscow ML). The other obvious differences is that many of the functions that operated on tuples in HOL88 operated on records in HOL98. This isn't a problem because the types of these functions will tell you the names of the record fields - which is pretty much all you need to know.

How do I get HOL for my Computer?

Before you can build HOL98 you first need to install Moscow ML. Details of how to get Moscow ML and which version to get, as well as how to get HOL98 are available from the Cambridge FTP area for HOL.

HOL Resources on the Net

Mailing Lists

The Info HOL mailing list dedicated to discussions about the HOL system. Users often ask questions there and its a friendly, low-traffic list, so you should feel welcome to ask questions as well. To join the list send mail to info-hol-request@lal.cs.byu.edu. You can send messages to the list by mailing info-hol@lal.cs.byu.edu. Perhaps your question has been asked before, there is an a archive of messages to this list.

Translating HOL88 Material to HOL98

HOL Reference Material on the Web

A searchable database built by the Laboratory for Applied Logic is available from two different sites (with two different interfaces).

Note, this reference material is for HOL88.

You can also download a PostScript version of the HOL98 User's Manual from its author Konrad Slind. Its not finished yet though.

HOL Tutorial Material on the Web

Other HOL Information Sites

_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [COMP8033] [ML] [HOL] [Exercises] [Lectures] [Assignments]
_____________________________________________________________________
Feedback & Queries: Jim.Grundy@anu.edu.au
Date Last Modified: Wed 22 Mar 2000
Universal Resource Locator: http://cs.anu.edu.au/student/comp8033/hol.html
Copyright © 2000 The Australian National University
All rights reserved