1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
<html>
<head><title>ACKNOWLEDGMENTS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACKNOWLEDGMENTS</h2>some contributors to the well-being of ACL2
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<p>
The development of ACL2 was initially made possible by funding from the
U. S. Department of Defense, including ARPA and ONR. We thank all the
organizations that have contributed support, including the following (in
alphabetical order).
<blockquote><p>
o AMD, for providing significant time over several years for Matt Kaufmann
to carry out ACL2 research, support, and development<br>
o Computational Logic, Inc. and its president, Don Good, where the first
eight years of ACL2 development occurred<br>
o DARPA<br>
o Digital Equipment Corporation<br>
o EDS, which provided some time for Matt Kaufmann's ACL2 work 1998-1999<br>
o IBM<br>
o NSF<br>
o ONR<br>
o Rockwell Collins<br>
o SRC<br>
o Sun Microsystems<br>
o University of Texas at Austin (in particular support to J Moore through
the Admiral B. R. Inman Chair of Computing Theory)<p>
</blockquote>
ACL2 was started in August, 1989 by Boyer and Moore working
together. They co-authored the first versions of axioms.lisp and
basis.lisp, with Boyer taking the lead in the formalization of
``<a href="STATE.html">state</a>'' and the most primitive <a href="IO.html">io</a> functions. Boyer also
had a significant hand in the development of the early versions of
the files interface-raw.lisp and translate.lisp. For several years,
Moore alone was responsible for developing the ACL2 system code,
though he consulted often with both Boyer and Kaufmann. In August,
1993, Kaufmann became jointly responsible with Moore for developing
the system. Boyer has continued to provide valuable consulting on
an informal basis.<p>
Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements. In particular, the <code>:cases</code> and
<code>:restrict</code> <a href="HINTS.html">hints</a> were his idea; he developed an early
version of congruence-based reasoning for Nqthm; and he helped in
the development of some early <a href="BOOKS.html">books</a> about arithmetic. In a
demonstration of his courage and faith in us, he pushed for
Computational Logic, Inc., to agree to the Motorola CAP contract --
which required formalizing a commercial DSP in the untested ACL2 --
and moved to Scottsdale, AZ, to do the work with the Motorola design
team. His demonstration of ACL2's utility was an inspiration, even
to those of us designing ACL2.<p>
John Cowles also helped in the development of some early <a href="BOOKS.html">books</a> about
arithmetic, and also provided valuable feedback and bug reports.<p>
Other early users of ACL2 at Computational Logic, Inc. helped
influence its development. In particular, Warren Hunt helped with
the port to Macintosh Common Lisp, and Art Flatau and Mike Smith
provided useful general feedback.<p>
Mike Smith helped develop the Emacs portion of the implementation of
proof trees.<p>
Bill Schelter made some enhancements to akcl (now gcl) that helped
to enhance ACL2 performance in that Common Lisp implementation, and
more generally, responded helpfully to our bug reports. Camm Maguire
has since provided wonderful gcl support, and has created a Debian package
for ACL2 built on GCL. We are also grateful to developers of other Common
Lisp implementations.<p>
Kent Pitman helped in our interaction with the ANSI Common Lisp
standardization committee, X3J13.<p>
John Cowles helped with the port to Windows (98) by answering
questions and running tests.<p>
Ruben Gamboa created a modification of ACL2 to allow reasoning about
the real numbers using non-standard analysis. His work has been
incorporated into the ACL2 distribution; see <a href="REAL.html">real</a>.<p>
Rob Sumners has made numerous useful suggestions. In particular, he
has designed and implemented improvements for <a href="STOBJ.html">stobj</a>s and been
key in our development of locally-bound stobjs; see <a href="NOTE-2-6.html">note-2-6</a>.<p>
Robert Krug has designed and implemented many changes in the
vicinity of the linear arithmetic package and its connection to
type-set and rewrite. He was also instrumental in the development of
<a href="EXTENDED-METAFUNCTIONS.html">extended-metafunctions</a>.<p>
Pete Manolios has made numerous useful suggestions. In particular, Pete
helped us to organize the first workshop and was a wonderful equal partner
with the two of us (Kaufmann and Moore) in producing the books that arose
from that workshop. Pete and his student, Daron Vroon, provided the current
implementation of <a href="ORDINALS.html">ordinals</a>.<p>
We also thank the contributors to the ACL2 workshops for some
suggested improvements and for the extensive collection of publicly
distributed benchmark problems. And we thank participants at the ACL2
seminar at the University of Texas for useful feedback.<p>
<em>Regarding the documentation:</em><p>
<blockquote>
Bill Young wrote significant portions of the <a href="ACL2-TUTORIAL.html">ACL2-TUTORIAL</a>
section of the ACL2 documentation, an important task for which we
are grateful. He, Bishop Brock, Rich Cohen, and Noah Friedman read
over considerable amounts of the documentation, and made many useful
comments. Others, particularly Bill Bevier and John Cowles, have
also made useful comments on the <a href="DOCUMENTATION.html">documentation</a>.<p>
Art Flatau helped develop the ACL2 <a href="MARKUP.html">markup</a> language and translators
from that language to Texinfo and HTML. Michael ``Bogo'' Bogomolny
created a search engine, beginning with Version 2.6, and for that
purpose modified the HTML translator to create one file per topic (a
good idea in any case).<p>
Laura Lawless provided many hours of help in marking up appropriate
parts of the <a href="DOCUMENTATION.html">documentation</a> in typewriter font.<p>
Noah Friedman developed an Emacs tool that helped us insert
``invisible links'' into the <a href="DOCUMENTATION.html">documentation</a>, which improve the
usability of that documentation under HTML readers such as Mosaic.<p>
Richard Stallman contributed a texinfo patch, to be found in the
file <code>doc/texinfo.tex</code>.</blockquote>
<p>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
