Major Section: MISCELLANEOUS
The development of ACL2 was made possible by funding from the U. S. Department of Defense, including ARPA and ONR.
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.
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 Manolios 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.
We also thank the contributors to the ACL2 workshops for some suggested improvements and for the extensive collection of publicly distributed benchmark problems.
Regarding the documentation:
Bill Young wrote significant portions of the ACL2-TUTORIAL 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 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.
Finally, we thank our employers for supporting the ACL2 project, including the University of Texas and the following corporations: Computational Logic, EDS, and Advanced Micro Devices. All of these institutions have been generous in providing us time to develop and improve ACL2, and they have supported our preference to keep ACL2 freely available to all.