1\chapter*{Riconoscimenti}\markboth{Riconoscimenti}{Riconoscimenti}
2
3La maggior parte di \HOL\ � basato su codice scritto da---in ordine
4alfabetico---%
5Hasan Amjad,
6Richard Boulton,
7Anthony Fox,
8Mike Gordon,
9Elsa Gunter,
10John Harrison,
11Peter Homeier,
12G\'erard Huet (e altri presso l'istituto 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,
27e
28Tjark Weber.
29Molti altri hanno fornito parti del sistema, correzione di bug, ecc.
30
31\subsection*{Edizione attuale}
32
33L'edizione attuale di tutti e quattro i volumi (\LOGIC, \TUTORIAL,
34\DESCRIPTION\ e \REFERENCE) � stata preparata da Michael Norrish e
35Konrad Slind. Altri contributi a questi volumi sono venuti da Hasan
36Amjad, che ha sviluppato una libreria di controllo del modello, e ha scritto le sezioni
37che ne descrivono l'uso; Jens Brandt, che ha sviluppato e documentato una
38libreria per i numeri razionali; Anthony Fox, che ha formalizzato e
39documentato nuove teorie dei gruppi riguardanti i word e le librerie associate; Mike
40Gordon, che ha documentato le librerie per i BDD e SAT; Peter Homeier,
41che ha implementato e documentato la libreria quoziente; Joe Hurd, che
42ha aggiunto materiale sulla ricerca della dimostrazione nel primo ordine; e Tjark Weber, che ha scritto
43le librerie per le Teorie Modulo Soddisfacibilit�~(SMT) e le Formule Booleane
44Quantificate~(QBF).
45
46\medskip
47
48Il materiale nella terza edizione costituisce un'approfondita rielaborazione
49ed estensione delle edizioni precedenti, l'unico pezzo essenzialmente non
50alterato � la semantica di Andy Pitts (in \LOGIC), il che riflette il fatto
51che, nonostante il sistema \HOL\ abbia subito uno sviluppo e un miglioramento
52continuo, la logica di \HOL\ � rimasta inalterata dalla sua prima edizione
53(1988).
54
55\newpage
56
57\subsection*{Seconda edizione}
58
59La seconda edizione di \REFERENCE\ � stato uno sforzo congiunto da parte del gruppo
60\HOL\ di Cambridge.
61
62\subsection*{Prima edizione}
63
64I tre volumi \TUTORIAL, \DESCRIPTION\ e \REFERENCE\ sono stati
65prodotti presso il Cambridge Research Center della SRI International con il
66supporto del DSTO Australia.
67
68Il progetto di documentazione di \HOL\ fu gestito da Mike Gordon, che
69scrisse anche parti di \DESCRIPTION\ e \TUTORIAL\ usando del materiale basato su
70uno scritto originario che descriveva il sistema \HOL\footnote{M.J.C.\ Gordon, `HOL:
71  a Proof Generating System for Higher Order Logic', in: {\it VLSI
72    Specification, Verification and Synthesis\/}, edito da G.\
73  Birtwistle e P.A.\ Subrahmanyam, (Kluwer Academic Publishers,
74  1988), pp.\ 73--128.} e {\sl The ML Handbook\/}\footnote{{\sl The
75    ML Handbook}, scritto inedito presso l'Inria da parte di Guy Cousineau, Mike
76  Gordon, G\'erard Huet, Robin Milner, Larry Paulson and Chris
77  Wadsworth.}. Altri che hanno contribuito a \DESCRIPTION\ includono Avra Cohn,
78che ha scritto del materiale su teoremi, regole, conversioni e tattiche,
79e ha anche composto l'indice (che fu battuto a macchina da Juanito Camilleri);
80Tom Melham, che ha scritto le sezioni che descrivono le definizioni di tipo,
81il concreto pacchetto dei tipi, e le tattiche di `risoluzione'; e Andy Pitts,
82che ha ideato la semantica a modelli insiemistici della logica di \HOL\ e ha scritto
83il materiale che la descrive.
84
85Il documento originario usava macro \LaTeX\ fornite da Elsa
86Gunter, Tom Melham e Larry Paulson. La battitura di tutti e tre
87i volumi fu gestita da Tom Melham. La copertina fu disegnata da Arnold
88Smith, che us� una fotografia di una `lanterna da neve' presa da
89Avra Cohn (nel cui giardino risiede l'oggetto originale). John Van
90Tassel ha composto l'immagine \LaTeX\ della lanterna.
91
92Molte altre persone oltre a quelle elencate di sopra hanno contribuito nello sforzo della
93documentazione di \HOL\, sia fornendo materiale, sia inviando elenchi di errori nella prima
94edizione. Grazie a tutti coloro che hanno aiutato, e grazie al DSTO e all'SRI per il loro
95generoso supporto.
96
97
98
99
100