1\chapter*{Acknowledgements}\markboth{Acknowledgements}{Acknowledgements}
2
3The bulk of \HOL\ is based on code written by---in alphabetical
4order---%
5Hasan Amjad,
6Richard Boulton,
7Anthony Fox,
8Mike Gordon,
9Elsa Gunter,
10John Harrison,
11Peter Homeier,
12G\'erard Huet (and others at INRIA),
13Joe Hurd,
14Ramana Kumar,
15Ken Friis Larsen,
16Tom Melham,
17Robin Milner,
18Lockwood Morris,
19Magnus Myreen,
20Malcolm Newey,
21Michael Norrish,
22Larry Paulson,
23Konrad Slind,
24Don Syme,
25Thomas T\"urk,
26Chris Wadsworth,
27and
28Tjark Weber.
29Many others have supplied parts of the system, bug fixes, etc.
30
31\subsection*{Current edition}
32
33The current edition of all four volumes (\LOGIC, \TUTORIAL,
34\DESCRIPTION\ and \REFERENCE) has been prepared by Michael Norrish and
35Konrad Slind. Further contributions to these volumes came from: Hasan
36Amjad, who developed a model checking library and wrote sections
37describing its use; Jens Brandt, who developed and documented a
38library for the rational numbers; Anthony Fox, who formalized and
39documented new word theories and the associated libraries; Mike
40Gordon, who documented the libraries for BDDs and SAT; Peter Homeier,
41who implemented and documented the quotient library; Joe Hurd, who
42added material on first order proof search; and Tjark Weber, who wrote
43libraries for Satisfiability Modulo Theories~(SMT) and Quantified
44Boolean Formulae~(QBF).
45
46\medskip
47
48The material in the third edition constitutes a thorough re-working
49and extension of previous editions.  The only essentially unaltered
50piece is the semantics by Andy Pitts (in \LOGIC), reflecting the fact
51that, although the \HOL\ system has undergone continual development
52and improvement, the \HOL\ logic is unchanged since the first edition
53(1988).
54
55\newpage
56
57\subsection*{Second edition}
58
59The second edition of \REFERENCE\ was a joint effort by the Cambridge
60\HOL\ group.
61
62\subsection*{First edition}
63
64The three volumes \TUTORIAL, \DESCRIPTION\ and \REFERENCE\ were
65produced at the Cambridge Research Center of SRI International with
66the support of DSTO Australia.
67
68The \HOL\ documentation project was managed by Mike Gordon, who also
69wrote parts of \DESCRIPTION\ and \TUTORIAL\ using material based on an
70early paper describing the \HOL\ system\footnote{M.J.C.\ Gordon, `HOL:
71  a Proof Generating System for Higher Order Logic', in: {\it VLSI
72    Specification, Verification and Synthesis\/}, edited by G.\
73  Birtwistle and P.A.\ Subrahmanyam, (Kluwer Academic Publishers,
74  1988), pp.\ 73--128.} and {\sl The ML Handbook\/}\footnote{{\sl The
75    ML Handbook}, unpublished report from Inria by Guy Cousineau, Mike
76  Gordon, G\'erard Huet, Robin Milner, Larry Paulson and Chris
77  Wadsworth.}.  Other contributers to \DESCRIPTION\ incude Avra Cohn,
78who contributed material on theorems, rules, conversions and tactics,
79and also composed the index (which was typeset by Juanito Camilleri);
80Tom Melham, who wrote the sections describing type definitions, the
81concrete type package and the `resolution' tactics; and Andy Pitts,
82who devised the set-theoretic semantics of the \HOL\ logic and wrote
83the material describing it.
84
85The original document design used \LaTeX\ macros supplied by Elsa
86Gunter, Tom Melham and Larry Paulson.  The typesetting of all three
87volumes was managed by Tom Melham.  The cover design is by Arnold
88Smith, who used a photograph of a `snow watching lantern' taken by
89Avra Cohn (in whose garden the original object resides).  John Van
90Tassel composed the \LaTeX\ picture of the lantern.
91
92Many people other than those listed above have contributed to the
93\HOL\ documentation effort, either by providing material, or by
94sending lists of errors in the first edition.  Thanks to everyone who
95helped, and thanks to DSTO and SRI for their generous support.
96
97\newpage
98\subsection*{In Memory of Mike Gordon}
99
100As 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.
101Mike 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.
102This 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.
103
104\bigskip
105\begin{center}
106Mike Gordon, 1948--2017
107\end{center}
108