1\chapter*{Preface}\markboth{Preface}{Preface}
2\label{intro}
3
4This volume contains the description of the \HOL\ system's logic.  It
5is one of four volumes making up the documentation for \HOL:
6
7\begin{myenumerate}
8\item \LOGIC: a formal description of the higher order logic
9  implemented by the \HOL{} system;
10\item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
11\item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
12\item \REFERENCE: the reference manual for \HOL.
13\end{myenumerate}
14
15\noindent These four documents will be referred to by the short names (in
16small slanted capitals) given above.
17
18This document, \LOGIC, serves as a formal definition of higher order
19logic in terms of a set-theoretic semantics.  This material was
20written by Andrew Pitts in 1991, and was originally part of
21\DESCRIPTION.  Because this logic is shared with other theorem-proving
22systems (HOL~Light, ProofPower), and is similar to that implemented in
23Isabelle, where it is called Isabelle/HOL, it is now presented in its
24own manual.
25
26The \HOL\ system is designed to support interactive theorem proving in
27higher order logic (hence the acronym `\HOL').  To this end, the formal
28logic is interfaced to a general purpose programming language (\ML, for
29meta-language) in which terms and theorems of the logic can be denoted,
30proof strategies expressed and applied, and logical theories developed.
31The version of higher order logic used in \HOL\ is predicate calculus
32with terms from the typed lambda calculus (\ie\ simple type
33theory). This was originally developed as a foundation for mathematics
34\cite{Church}.  The primary application area of \HOL\ was initially
35intended to be the specification and verification of hardware designs.
36(The use of higher order logic for this purpose was first advocated by
37Keith Hanna \cite{Hanna-Daeche}.)  However, the logic does not restrict
38applications to hardware; \HOL\ has been applied to many other areas.
39
40Thus, this document describes the theoretical underpinnings of the
41\HOL{} system, and presents it abstractly.
42
43The approach to mechanizing formal proof used in \HOL\ is due to Robin
44Milner \cite{Edinburgh-LCF}, who also headed the team that designed
45and implemented the language \ML.  That work centred on a system
46called \LCF\ (logic for computable functions), which was intended for
47interactive automated reasoning about higher order recursively defined
48functions.  The interface of the logic to the meta-language was made
49explicit, using the type structure of \ML, with the intention that
50other logics eventually be tried in place of the original logic.  The
51\HOL\ system is a direct descendant of \LCF; this is reflected in
52everything from its structure and outlook to its incorporation of \ML,
53and even to parts of its implementation.  Thus \HOL\ satisfies the
54early plan to apply the \LCF\ methodology to other logics.
55
56The original \LCF\ was implemented at Edinburgh in the early 1970's, and is now
57referred to as `Edinburgh \LCF'. Its code was ported from Stanford Lisp to
58Franz Lisp by G\'erard Huet at {\small INRIA}, and was used in a French
59research project called `Formel'.  Huet's Franz Lisp version of \LCF\ was
60further developed at Cambridge by Larry Paulson, and became known as `Cambridge
61\LCF'. The \HOL\ system is implemented on top of an early version of Cambridge
62\LCF\ and consequently many features of both Edinburgh and Cambridge \LCF\ were
63inherited by \HOL. For example, the axiomatization of higher order logic used
64is not the classical one due to Church, but an equivalent formulation
65influenced by \LCF.
66
67An enhanced and rationalized version of \HOL, called \HOL 88, was
68released (in 1988), after the original \HOL\ system had been in use
69for several years.  \HOL 90 (released in 1990) was a port of \HOL 88
70to SML \cite{sml} by Konrad Slind at the University of Calgary. It has
71been further developed through the 1990's. \HOL{} 4 is the latest
72version of \HOL, and is also implemented in SML; it features a number
73of novelties compared to its predecessors.  \HOL{} 4 is also the
74supported version of the system for the international \HOL\ community.
75
76We have retroactively decided to number \HOL{} implementations in the
77following way
78\begin{enumerate}
79\item \HOL88 and earlier: implementations based on a Lisp substrate,
80  with Classic ML.
81\item \HOL90: implementations in Standard ML, principally using the
82  SML/NJ implementation.
83\item \HOL98 (Athabasca and Taupo releases): implementations using
84  Moscow ML, and with a new library and theory mechanism.
85\item \HOL{} (Kananaskis releases)
86\end{enumerate}
87Therefore, with \HOL{}~4, we do away with the habit of associating
88implementations with year numbers.  Individual releases within
89\HOL{}~4 will retain the \textit{lake-number} naming scheme.
90
91In this document, the acronym `\HOL' refers to both the interactive theorem
92proving system and to the version of higher order logic that the system
93supports; where there is serious ambiguity, the former is called `the \HOL\
94system' and the latter `the \HOL\ logic'.
95
96
97%%% Local Variables:
98%%% mode: latex
99%%% TeX-master: "logic"
100%%% End:
101