|
|
|---|
|
|
|
|---|
Some contributors to the well-being of ACL2
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).
Regarding DARPA support: We thank DARPA for approving release of the following documentation topics and support with “DISTRIBUTION STATEMENT A. Approved for public release. Distribution is unlimited.”
Regarding NSF support:
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
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.
ACL2 depends on the availability of robust Common Lisp implementations, so we are grateful to the developers of those implementations. Early in ACL2's history, 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. Gary Byers and R. Matthew Emerson have continually improved Clozure Common Lisp (CCL), often based on feedback from the ACL2 community. 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, Sol Swords, and David Rager have our gratitude for starting the ACL2+Books repository.
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, applicative hash tables, and a function memoization mechanism to facilitate reuse of previously computed results. Subsequently, Jared Davis and Sol Swords made further contributions. We thank them all for this work, most of which has been incorporated into ACL2; see hons-and-memoization.
Other contributions to the ACL2 system continue to be made by members of the ACL2 community. In particular, following the first Developers Workshop in May, 2017 through the time of this writing in November, 2019, such contributors include Alessandro Coglio, Keshav Kini, Mihir Mehta, Pete Manolios, and especially Sol Swords, while Eric Smith and many others have suggested changes that we have implemented, often by providing helpful examples. The release-notes detail such contributions as well as many suggestions from the community for improvements that we ultimately implemented.
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-tutorial section 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 in which ACL2 documentation was originally developed, along with 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 .Jared Davis created the xdoc system that is now the basis not only for the ACL2 system documentation (file
books/system/doc/acl2-doc.lisp ), but also for the community-books documentation.
We thank Blake Grugett for designing the current version of the ACL2 logo (which for example appears on the ACL2 home page), based on an original design created in the 1990s by Computational Logic, Inc.