\chapter*{Riconoscimenti}\markboth{Riconoscimenti}{Riconoscimenti}

La maggior parte di \HOL\ è basato su codice scritto da---in ordine
alfabetico---%
Hasan Amjad,
Richard Boulton,
Anthony Fox,
Mike Gordon,
Elsa Gunter,
John Harrison,
Peter Homeier,
G\'erard Huet (e altri presso l'istituto 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,
e
Tjark Weber.
Molti altri hanno fornito parti del sistema, correzione di bug, ecc.

\subsection*{Edizione attuale}

L'edizione attuale di tutti e quattro i volumi (\LOGIC, \TUTORIAL,
\DESCRIPTION\ e \REFERENCE) è stata preparata da Michael Norrish e
Konrad Slind. Altri contributi a questi volumi sono venuti da Hasan
Amjad, che ha sviluppato una libreria di controllo del modello, e ha scritto le sezioni
che ne descrivono l'uso; Jens Brandt, che ha sviluppato e documentato una
libreria per i numeri razionali; Anthony Fox, che ha formalizzato e
documentato nuove teorie dei gruppi riguardanti i word e le librerie associate; Mike
Gordon, che ha documentato le librerie per i BDD e SAT; Peter Homeier,
che ha implementato e documentato la libreria quoziente; Joe Hurd, che
ha aggiunto materiale sulla ricerca della dimostrazione nel primo ordine; e Tjark Weber, che ha scritto
le librerie per le Teorie Modulo Soddisfacibilità~(SMT) e le Formule Booleane
Quantificate~(QBF).

\medskip

Il materiale nella terza edizione costituisce un'approfondita rielaborazione
ed estensione delle edizioni precedenti, l'unico pezzo essenzialmente non
alterato è la semantica di Andy Pitts (in \LOGIC), il che riflette il fatto
che, nonostante il sistema \HOL\ abbia subito uno sviluppo e un miglioramento
continuo, la logica di \HOL\ è rimasta inalterata dalla sua prima edizione
(1988).

\newpage

\subsection*{Seconda edizione}

La seconda edizione di \REFERENCE\ è stato uno sforzo congiunto da parte del gruppo
\HOL\ di Cambridge.

\subsection*{Prima edizione}

I tre volumi \TUTORIAL, \DESCRIPTION\ e \REFERENCE\ sono stati
prodotti presso il Cambridge Research Center della SRI International con il
supporto del DSTO Australia.

Il progetto di documentazione di \HOL\ fu gestito da Mike Gordon, che
scrisse anche parti di \DESCRIPTION\ e \TUTORIAL\ usando del materiale basato su
uno scritto originario che descriveva il sistema \HOL\footnote{M.J.C.\ Gordon, `HOL:
  a Proof Generating System for Higher Order Logic', in: {\it VLSI
    Specification, Verification and Synthesis\/}, edito da G.\
  Birtwistle e P.A.\ Subrahmanyam, (Kluwer Academic Publishers,
  1988), pp.\ 73--128.} e {\sl The ML Handbook\/}\footnote{{\sl The
    ML Handbook}, scritto inedito presso l'Inria da parte di Guy Cousineau, Mike
  Gordon, G\'erard Huet, Robin Milner, Larry Paulson and Chris
  Wadsworth.}. Altri che hanno contribuito a \DESCRIPTION\ includono Avra Cohn,
che ha scritto del materiale su teoremi, regole, conversioni e tattiche,
e ha anche composto l'indice (che fu battuto a macchina da Juanito Camilleri);
Tom Melham, che ha scritto le sezioni che descrivono le definizioni di tipo,
il concreto pacchetto dei tipi, e le tattiche di `risoluzione'; e Andy Pitts,
che ha ideato la semantica a modelli insiemistici della logica di \HOL\ e ha scritto
il materiale che la descrive.

Il documento originario usava macro \LaTeX\ fornite da Elsa
Gunter, Tom Melham e Larry Paulson. La battitura di tutti e tre
i volumi fu gestita da Tom Melham. La copertina fu disegnata da Arnold
Smith, che usò una fotografia di una `lanterna da neve' presa da
Avra Cohn (nel cui giardino risiede l'oggetto originale). John Van
Tassel ha composto l'immagine \LaTeX\ della lanterna.

Molte altre persone oltre a quelle elencate di sopra hanno contribuito nello sforzo della
documentazione di \HOL\, sia fornendo materiale, sia inviando elenchi di errori nella prima
edizione. Grazie a tutti coloro che hanno aiutato, e grazie al DSTO e all'SRI per il loro
generoso supporto.