Major Section: MISCELLANEOUS
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).
o AMD, for providing significant time over several years for Matt Kaufmann to carry out ACL2 research, support, and development
o Computational Logic, Inc. and its president, Don Good, where the first eight years of ACL2 development occurred
o Centaur Technology
o DARPA
o Digital Equipment Corporation
o EDS, which provided some time for Matt Kaufmann's ACL2 work 1998-1999
o ForrestHunt and, more generally, Warren A. Hunt, Jr. (see below)
o IBM
o NSF
o ONR
o Rockwell Collins
o SRC
o Sun Microsystems
o University of Texas at Austin (in particular support to J Moore through the Admiral B. R. Inman Chair of Computing Theory)
We are especially grateful to Warren A. Hunt, Jr. for his unrivaled efforts in securing support for the entire ACL2 research group at both Computational Logic, Inc., and the University of Texas at Austin. Without his efforts, we would have spent less time working on the system and fewer students would have been funded to apply it.
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 ``state'' and the most primitive io 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.
Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements. In particular, the :cases and
:restrict hints were his idea; he developed an early version of
congruence-based reasoning for Nqthm; and he helped in the development of
some early books 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.
John Cowles also helped in the development of some early books about arithmetic, and also provided valuable feedback and bug reports.
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.
Mike Smith helped develop the Emacs portion of the implementation of proof trees.
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.
Kent Pitman helped in our interaction with the ANSI Common Lisp standardization committee, X3J13.
John Cowles helped with the port to Windows (98) by answering questions and running tests.
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 real.
Rob Sumners has made numerous useful suggestions. In particular, he has designed and implemented improvements for stobjs and been key in our development of locally-bound stobjs; see note-2-6.
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 extended-metafunctions.
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 ordinals.
Jared Davis and Sol Swords have our gratitude for starting the acl2-books repository, http://acl2-books.googlecode.com/.
We thank David L. Rager for contributing an initial version of the support for parallelism in an experimental extension of ACL2.
Bob Boyer and Warren A. Hunt, Jr. developed a canonical representation for ACL2 data objects and a function memoization mechanism to facilitate reuse of previously computed results. We thank them for their extensive efforts for the corresponding experimental (as of 2008 and 2009) extension of ACL2; see hons-and-memoization.
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. More generally, we thank the ACL2 community for feedback, contributed books (see community-books), and their interest in the ACL2 project.
Regarding the documentation:
Bill Young wrote significant portions of the original
acl2-tutorialsection of the ACL2 documentation, including what is now called alternative-introduction. This was an especially important task in the early years when there was no guide for how to use ACL2 and we are very 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 documentation.Art Flatau helped develop the ACL2 markup 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).
Laura Lawless provided many hours of help in marking up appropriate parts of the documentation in typewriter font.
Noah Friedman developed an Emacs tool that helped us insert ``invisible links'' into the documentation, which improve the usability of that documentation under HTML readers such as Mosaic.
Richard Stallman contributed a texinfo patch, to be found in the file
doc/texinfo.tex.
