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