@article(congruence,
 author       = "Bishop Brock and Matt Kaufmann and {J Strother} Moore",
 year         = "2008",
 title        = "Rewriting with Equivalence Relations in ACL2",
 journal      = "Journal of Automated Reasoning",
 volume       = "40",
 number       = "4",
 pages        = "293--306",
 doi          = "10.1007/s10817-007-9095-9",
)
@misc(acl2-books-svn,
 author       = "The {ACL2} community",
 title        = "{{ACL2} Community Books}",
 note         = "See URL \url {https://code.google.com/p/acl2-books/}",
)
@misc(acl2-users-manual,
 author       = "Matt Kaufmann and J Strother Moore",
 title        = "{ACL2} User's Manual",
 note         = "See URL \url {http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html}",
)
@misc(patterned-congruence-rules,
 author       = "Matt Kaufmann and J Strother Moore",
 title        = "Rough Diamond: An Extension of Equivalence-based Rewriting",
 note         = "To appear, Proceedings of ITP 2014",
)
@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",
)
@inproceedings(EPTCS114.1,
 author       = "Matt Kaufmann and J Strother Moore",
 year         = "2013",
 title        = "Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1",
 editor       = "Ruben Gamboa and Jared Davis",
 booktitle    = "{\rm Proceedings International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Laramie, Wyoming, USA , May 30-31, 2013}",
 series       = "Electronic Proceedings in Theoretical Computer Science",
 volume       = "114",
 publisher    = "Open Publishing Association",
 pages        = "5--12",
 doi          = "10.4204/EPTCS.114.1",
)