\chapter*{Preface}\markboth{Preface}{Preface}
\label{intro}

This volume contains the  description of  the \HOL\  system.
It is one of four volumes making up the documentation for \HOL:

\begin{myenumerate}
\item \LOGIC: a formal description of the higher order logic
  implemented by the \HOL{} system;
\item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
\item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
\item \REFERENCE: the reference manual for \HOL.
\end{myenumerate}

\noindent These four documents will be referred to by the short names (in
small slanted capitals) given above.

This document, \DESCRIPTION, is an advanced guide for users with some
prior experience of the system.  Beginners should start with the
companion document \TUTORIAL.

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 (\ie\ simple type
theory). This was originally developed as a foundation for mathematics
\cite{Church}.  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 \cite{Hanna-Daeche}.)  However, the logic does not restrict
applications to hardware; \HOL\ has been applied to many other areas.

This document presents the \HOL\ logic in its \ML{} guise, and
explains the means by which meta-language functions can be used to
generate proofs in the logic.  Thus, it describes how the abstract
system of \LOGIC{} is actually implemented in the \ML{} programming
language, providing comprehensive descriptions of the system's major
features.

The approach to mechanizing formal proof used in \HOL\ is due to Robin Milner
\cite{Edinburgh-LCF}, 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\'erard Huet at {\small 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.

An enhanced and rationalized version of \HOL, called \HOL 88, was
released (in 1988), after the original \HOL\ system had been in use
for several years.  \HOL 90 (released in 1990) was a port of \HOL 88
to SML \cite{sml} by Konrad Slind at the University of Calgary. It has
been further developed through the 1990's. \HOL{} 4 is the latest
version of \HOL, and is also implemented in SML; it features a number
of novelties compared to its predecessors.  \HOL{} 4 is also the
supported version of the system for the international \HOL\ community.

We have retroactively decided to number \HOL{} implementations in the
following way
\begin{enumerate}
\item \HOL88 and earlier: implementations based on a Lisp substrate,
  with Classic ML.
\item \HOL90: implementations in Standard ML, principally using the
  SML/NJ implementation.
\item \HOL98 (Athabasca and Taupo releases): implementations using
  Moscow ML, and with a new library and theory mechanism.
\item \HOL{} (Kananaskis releases)
\end{enumerate}
Therefore, with \HOL{}~4, we do away with the habit of associating
implementations with year numbers.  Individual releases within
\HOL{}~4 will retain the \textit{lake-number} naming scheme.

In this document, the acronym `\HOL' refers to both the interactive theorem
proving system and to the version of higher order logic that the system
supports; where there is serious ambiguity, the former is called `the \HOL\
system' and the latter `the \HOL\ logic'.


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "description"
%%% End: