@misc(04-austel-typing,
 author       = {Vernon Austel},
 year         = {2004},
 title        = {Adding a typing mechanism to {ACL2}},
 howpublished = {ACL2 '04},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/austel/acl2-types.pdf},
)
@incollection(02-boyer-stobjs,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {2002},
 title        = {Single-Threaded Objects in {ACL2}},
 booktitle    = {Practical Aspects of Declarative Languages},
 series       = {LNCS},
 volume       = {2257},
 publisher    = {Springer},
 pages        = {9--27},
 doi          = {10.1007/3-540-45587-6\_3},
)
@misc(97-brock-defstructure,
 author       = {Bishop Brock},
 year         = {1997},
 title        = {Defstructure for {ACL2}},
 url          = {http://www.cs.utexas.edu/users/moore/publications/others/defstructure-brock.ps},
)
@inproceedings(14-harsh-defdata,
 author       = {Harsh Raju Chamarthi and Peter C. Dillinger and Panagiotis Manolios},
 year         = {2014},
 title        = {Data Definitions in the ACL2 Sedan},
 booktitle    = {ACL2 '14},
 publisher    = {EPTCS},
 pages        = {27--48},
 doi          = {10.4204/EPTCS.152.3},
)
@misc(04-davis-osets,
 author       = {Jared Davis},
 year         = {2004},
 title        = {Finite Set Theory based on Fully Ordered Lists},
 howpublished = {ACL2 '04},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/davis/set-theory.pdf},
)
@inproceedings(06-davis-memories,
 author       = {Jared Davis},
 year         = {2006},
 title        = {Memories: Array-like records for {ACL2}},
 booktitle    = {ACL2 '06},
 publisher    = {ACM},
 pages        = {57--60},
 doi          = {10.1145/1217975.1217986},
)
@inproceedings(14-centaur-ucode,
 author       = {Jared Davis and Anna Slobodova and Sol Swords},
 year         = {2014},
 title        = {Microcode Verification: Another Piece of the Microprocessor Verification Puzzle},
 booktitle    = {ITP '14},
 series       = {LNCS},
 volume       = {8558},
 publisher    = {Springer},
 pages        = {1--16},
 doi          = {10.1007/978-3-319-08970-6\_1},
)
@misc(fty-xdoc,
 author       = {Jared Davis and Sol Swords},
 year         = {2015},
 title        = {{XDOC} Documentation for {FTY}},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/manuals/},
)
@inproceedings(13-gastel-xmas,
 author       = {Bernard van Gastel and Julien Schmaltz},
 year         = {2013},
 title        = {A formalisation of {XMAS}},
 booktitle    = {ACL2 '13},
 publisher    = {EPTCS},
 pages        = {111--126},
 doi          = {10.4204/EPTCS.114.9},
)
@inproceedings(13-goel-stobjs,
 author       = {Shilpi Goel and {Hunt, Jr.}, Warren A. and Matt Kaufmann},
 year         = {2013},
 title        = {Abstract Stobjs and their application to {ISA} modeling},
 booktitle    = {ACL2 '13},
 publisher    = {EPTCS},
 pages        = {54--69},
 doi          = {10.4204/EPTCS.114.5},
)
@misc(03-greve-typedrecords,
 author       = {David Greve and Matthew Wilding},
 year         = {2003},
 title        = {Typed ACL2 Records},
 howpublished = {ACL2 '03},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/greve-wilding_defrecord/defrecord.pdf},
)
@article(07-greve-efficient,
 author       = {David A. Greve and Matt Kaufmann and Panagiotis Manolios and J Strother Moore and Sandip Ray and Ruiz-Reina, Jos\'{e} Luis and Rob Sumners and Daron Vroon and Matthew Wilding},
 year         = {2008},
 title        = {Efficient execution in an automated reasoning environment},
 journal      = {Journal of Functional Programming},
 volume       = {18},
 pages        = {15--46},
 doi          = {10.1017/S0956796807006338},
)
@inproceedings(14-hardin-llvm,
 author       = {David S. Hardin and Jennifer A. Davis and David A. Greve and Jedidiah R. McClurg},
 year         = {2014},
 title        = {Development of a Translator from {LLVM} to {ACL2}},
 booktitle    = {ACL2 '14},
 publisher    = {EPTCS},
 pages        = {163--177},
 doi          = {10.4204/EPTCS.152.13},
)
@misc(02-kaufmann-records,
 author       = {Matt Kaufmann and Rob Sumners},
 year         = {2002},
 title        = {Efficient Rewriting of Data Structures in {ACL2}},
 howpublished = {ACL2 '02},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/contrib/kaufmann-sumners/rcd.pdf},
)
@article(99-lamport-typed,
 author       = {Leslie Lamport and Lawrence C. Paulson},
 year         = {1999},
 title        = {Should Your Specification Language Be Typed},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {21},
 number       = {3},
 pages        = {502--526},
 doi          = {10.1145/319301.319317},
)
@book(65-morse-sets,
 author       = {Anthony P. Morse},
 year         = {1965},
 title        = {A Theory of Sets},
 publisher    = {Academic Press},
)
@inproceedings(14-selfridge-polymorphic,
 author       = {Benjamin Selfridge and Eric Smith},
 year         = {2014},
 title        = {Polymorphic Types in {ACL2}},
 booktitle    = {ACL2 '14},
 publisher    = {EPTCS},
 pages        = {49--60},
 doi          = {10.4204/EPTCS.152.4},
)
@inproceedings(11-swords-gl,
 author       = {Sol Swords and Jared Davis},
 year         = {2011},
 title        = {Bit-Blasting {ACL2} Theorems},
 booktitle    = {ACL2 '11},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {70},
 pages        = {84--102},
 doi          = {10.4204/EPTCS.70.7},
)