@misc(acl2-books-svn,
 author       = "The~{ACL2} community",
 title        = "{{ACL2} Community Books}",
 note         = "See URL \url {https://code.google.com/p/acl2-books/}",
)
@inproceedings(defabsstobj-paper,
 author       = "Shilpi Goel and Warren A.~Hunt, Jr. and Matt Kaufmann",
 year         = "2013",
 title        = "Abstract Stobjs and Their Application to ISA Modeling",
 booktitle    = "Proceedings 11th International Workshop on the ACL2 Theorem Prover and its Applications",
)
@misc(release-notes-doc,
 author       = "Matt Kaufmann and J~Strother Moore",
 title        = "{ACL2} documentation topic: {RELEASE-NOTES}",
 note         = "See URL \url {http://www.cs.utexas.edu/users/moore/acl2/current/RELEASE-NOTES.html}",
)
@misc(how-to-make-patches,
 author       = "Matt Kaufmann and J~Strother Moore",
 title        = "Instructions for modifying {ACL2} system code",
 note         = "See URL \url {http://www.cs.utexas.edu/users/moore/acl2/open-architecture/how-to-make-patches.txt}",
)
@inproceedings(DBLP:journals/corr/abs-1110-4673,
 author       = "Matt Kaufmann and J~Strother Moore",
 year         = "2011",
 title        = "How Can I Do That with ACL2? Recent Enhancements to ACL2",
 editor       = "David Hardin and Julien Schmaltz",
 booktitle    = "ACL2",
 series       = "EPTCS",
 volume       = "70",
 pages        = "46--60",
 url          = "http://dx.doi.org/10.4204/EPTCS.70.4",
)
@book(Steele:1990:CLL:95411,
 author       = "Guy~L. Steele, Jr.",
 year         = "1990",
 title        = "Common LISP: the language (2nd ed.)",
 publisher    = "Digital Press",
 address      = "Newton, MA, USA",
)