\chapter*{Acknowledgements}\markboth{Acknowledgements}{Acknowledgements}

The bulk of \HOL\ is based on code written by---in alphabetical
order---%
Hasan Amjad,
Richard Boulton,
Anthony Fox,
Mike Gordon,
Elsa Gunter,
John Harrison,
Peter Homeier,
G\'erard Huet (and others at INRIA),
Joe Hurd,
Ramana Kumar,
Ken Friis Larsen,
Tom Melham,
Robin Milner,
Lockwood Morris,
Magnus Myreen,
Malcolm Newey,
Michael Norrish,
Larry Paulson,
Konrad Slind,
Don Syme,
Thomas T\"urk,
Chris Wadsworth,
and
Tjark Weber.
Many others have supplied parts of the system, bug fixes, etc.

\subsection*{Current edition}

The current edition of all four volumes (\LOGIC, \TUTORIAL,
\DESCRIPTION\ and \REFERENCE) has been prepared by Michael Norrish and
Konrad Slind. Further contributions to these volumes came from: Hasan
Amjad, who developed a model checking library and wrote sections
describing its use; Jens Brandt, who developed and documented a
library for the rational numbers; Anthony Fox, who formalized and
documented new word theories and the associated libraries; Mike
Gordon, who documented the libraries for BDDs and SAT; Peter Homeier,
who implemented and documented the quotient library; Joe Hurd, who
added material on first order proof search; and Tjark Weber, who wrote
libraries for Satisfiability Modulo Theories~(SMT) and Quantified
Boolean Formulae~(QBF).

\medskip

The material in the third edition constitutes a thorough re-working
and extension of previous editions.  The only essentially unaltered
piece is the semantics by Andy Pitts (in \LOGIC), reflecting the fact
that, although the \HOL\ system has undergone continual development
and improvement, the \HOL\ logic is unchanged since the first edition
(1988).

\newpage

\subsection*{Second edition}

The second edition of \REFERENCE\ was a joint effort by the Cambridge
\HOL\ group.

\subsection*{First edition}

The three volumes \TUTORIAL, \DESCRIPTION\ and \REFERENCE\ were
produced at the Cambridge Research Center of SRI International with
the support of DSTO Australia.

The \HOL\ documentation project was managed by Mike Gordon, who also
wrote parts of \DESCRIPTION\ and \TUTORIAL\ using material based on an
early paper describing the \HOL\ system\footnote{M.J.C.\ Gordon, `HOL:
  a Proof Generating System for Higher Order Logic', in: {\it VLSI
    Specification, Verification and Synthesis\/}, edited by G.\
  Birtwistle and P.A.\ Subrahmanyam, (Kluwer Academic Publishers,
  1988), pp.\ 73--128.} and {\sl The ML Handbook\/}\footnote{{\sl The
    ML Handbook}, unpublished report from Inria by Guy Cousineau, Mike
  Gordon, G\'erard Huet, Robin Milner, Larry Paulson and Chris
  Wadsworth.}.  Other contributers to \DESCRIPTION\ incude Avra Cohn,
who contributed material on theorems, rules, conversions and tactics,
and also composed the index (which was typeset by Juanito Camilleri);
Tom Melham, who wrote the sections describing type definitions, the
concrete type package and the `resolution' tactics; and Andy Pitts,
who devised the set-theoretic semantics of the \HOL\ logic and wrote
the material describing it.

The original document design used \LaTeX\ macros supplied by Elsa
Gunter, Tom Melham and Larry Paulson.  The typesetting of all three
volumes was managed by Tom Melham.  The cover design is by Arnold
Smith, who used a photograph of a `snow watching lantern' taken by
Avra Cohn (in whose garden the original object resides).  John Van
Tassel composed the \LaTeX\ picture of the lantern.

Many people other than those listed above have contributed to the
\HOL\ documentation effort, either by providing material, or by
sending lists of errors in the first edition.  Thanks to everyone who
helped, and thanks to DSTO and SRI for their generous support.

\newpage
\subsection*{In Memory of Mike Gordon}

As documented in the academic literature, in material available from his archived web-pages at the University of Cambridge Computer Laboratory, and in these manuals, Mike Gordon was \HOL's primary creator and developer.
Mike not only created a significant piece of software, inspiring this and many other projects since, but also built a world-leading research group in the Computer Laboratory.
This research environment was wonderfully productive for many of the system's authors, and we all owe Mike an enormous debt for both the original work on \HOL, and for the way he and his group supported our own development as researchers and \HOL{} hackers.

\bigskip
\begin{center}
Mike Gordon, 1948--2017
\end{center}