Robert S. Boyer & J Strother Moore (2002):
Single-Threaded Objects in ACL2.
In: Practical Aspects of Declarative Languages,
LNCS 2257.
Springer,
pp. 9–27,
doi:10.1007/3-540-45587-6_3.
Harsh Raju Chamarthi, Peter C. Dillinger & Panagiotis Manolios (2014):
Data Definitions in the ACL2 Sedan.
In: ACL2 '14.
EPTCS,
pp. 27–48,
doi:10.4204/EPTCS.152.3.
Jared Davis (2006):
Memories: Array-like records for ACL2.
In: ACL2 '06.
ACM,
pp. 57–60,
doi:10.1145/1217975.1217986.
Jared Davis, Anna Slobodova & Sol Swords (2014):
Microcode Verification: Another Piece of the Microprocessor Verification Puzzle.
In: ITP '14,
LNCS 8558.
Springer,
pp. 1–16,
doi:10.1007/978-3-319-08970-6_1.
Bernard van Gastel & Julien Schmaltz (2013):
A formalisation of XMAS.
In: ACL2 '13.
EPTCS,
pp. 111–126,
doi:10.4204/EPTCS.114.9.
Shilpi Goel, Warren A. Hunt, Jr. & Matt Kaufmann (2013):
Abstract Stobjs and their application to ISA modeling.
In: ACL2 '13.
EPTCS,
pp. 54–69,
doi:10.4204/EPTCS.114.5.
David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José Luis Ruiz-Reina, Rob Sumners, Daron Vroon & Matthew Wilding (2008):
Efficient execution in an automated reasoning environment.
Journal of Functional Programming 18,
pp. 15–46,
doi:10.1017/S0956796807006338.
David S. Hardin, Jennifer A. Davis, David A. Greve & Jedidiah R. McClurg (2014):
Development of a Translator from LLVM to ACL2.
In: ACL2 '14.
EPTCS,
pp. 163–177,
doi:10.4204/EPTCS.152.13.
Leslie Lamport & Lawrence C. Paulson (1999):
Should Your Specification Language Be Typed.
ACM Transactions on Programming Languages and Systems 21(3),
pp. 502–526,
doi:10.1145/319301.319317.
Anthony P. Morse (1965):
A Theory of Sets.
Academic Press.
Benjamin Selfridge & Eric Smith (2014):
Polymorphic Types in ACL2.
In: ACL2 '14.
EPTCS,
pp. 49–60,
doi:10.4204/EPTCS.152.4.
Sol Swords & Jared Davis (2011):
Bit-Blasting ACL2 Theorems.
In: ACL2 '11,
Electronic Proceedings in Theoretical Computer Science 70,
pp. 84–102,
doi:10.4204/EPTCS.70.7.