@article(brockdefstructure,
 author       = "Bishop Brock",
 title        = "Defstructure for ACL2, 1997",
 url          = "http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html\#Data-Structures",
)
@inproceedings(acl2-11,
 author       = "Harsh Raju Chamarthi and Peter C. Dillinger and Matt Kaufmann and Panagiotis Manolios",
 year         = "2011",
 title        = "Integrating Testing and Interactive Theorem Proving",
 editor       = "David Hardin and Julien Schmaltz",
 booktitle    = "ACL2",
 series       = "EPTCS",
 volume       = "70",
 pages        = "4--19",
 url          = "http://dx.doi.org/10.4204/EPTCS.70.1",
)
@inproceedings(chamarthi2011automated,
 author       = "Harsh Raju Chamarthi and Panagiotis Manolios",
 year         = "2011",
 title        = "Automated specification analysis using an interactive theorem prover",
 editor       = "Per Bjesse and Anna Slobodov{\'a}",
 booktitle    = "FMCAD",
 publisher    = "FMCAD Inc.",
 pages        = "46--53",
 url          = "http://dl.acm.org/citation.cfm?id=2157665",
)
@manual(Davis/util,
 author       = "Jared C. Davis",
 title        = "Std/util Documentation",
 url          = "http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____STD_F2UTIL",
)
@article(DBLP:journals/jfp/GreveKMMRRSVW08,
 author       = "David A. Greve and Matt Kaufmann and Panagiotis Manolios and J. Strother Moore and Sandip Ray and Jos{\'e}-Luis Ruiz-Reina and Rob Sumners and Daron Vroon and Matthew Wilding",
 year         = "2008",
 title        = "Efficient execution in an automated reasoning environment",
 journal      = "J. Funct. Program.",
 volume       = "18",
 number       = "1",
 pages        = "15--46",
 url          = "http://dx.doi.org/10.1017/S0956796807006338",
)
@book(car,
 author       = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
 year         = "2000",
 title        = "Computer-Aided Reasoning: An Approach",
 publisher    = "Kluwer Academic Publishers",
 doi          = "10.1007/978-1-4757-3188-0",
)
@inproceedings(enhancementsKM13,
 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",
)
@inproceedings(02-kaufmann-rewriting,
 author       = "Matt Kaufmann and Rob Sumners",
 year         = "2002",
 title        = "Efficient Rewriting of Operations on Finite Structures in {ACL2}",
 booktitle    = "Third International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 '02)",
)
@inproceedings(ManoliosKaufmann02,
 author       = "Panagiotis Manolios and Matt Kaufmann",
 year         = "2002",
 title        = "Adding a Total Order to {ACL2}",
 editor       = "Matt Kaufmann and J Strother Moore",
 booktitle    = "Proceedings of the {ACL2} Workshop 2002",
)
@inproceedings(ManoliosVroon2006,
 author       = "Panagiotis Manolios and Daron Vroon",
 year         = "2006",
 title        = "Termination Analysis with Calling Context Graphs",
 editor       = "Thomas Ball and Robert B. Jones",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "4144",
 publisher    = "Springer",
 pages        = "401--414",
 url          = "http://dx.doi.org/10.1007/11817963_36",
)
@manual(Swords:fty,
 author       = "Sol Swords",
 title        = "FixType Documentation",
 url          = "http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=FTY____FTY",
)
@inproceedings(swords2006soundness,
 author       = "Sol Swords and William R. Cook",
 year         = "2006",
 title        = "Soundness of the simply typed lambda calculus in ACL2",
 editor       = "Panagiotis Manolios and Matthew Wilding",
 booktitle    = "ACL2",
 publisher    = "ACM",
 pages        = "35--39",
 url          = "http://doi.acm.org/10.1145/1217975.1217982",
)