References

  1. Vernon Austel (2004): Adding a typing mechanism to ACL2. ACL2 '04. Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/austel/acl2-types.pdf.
  2. 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.
  3. Bishop Brock (1997): Defstructure for ACL2. Available at http://www.cs.utexas.edu/users/moore/publications/others/defstructure-brock.ps.
  4. 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.
  5. Jared Davis (2004): Finite Set Theory based on Fully Ordered Lists. ACL2 '04. Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/davis/set-theory.pdf.
  6. Jared Davis (2006): Memories: Array-like records for ACL2. In: ACL2 '06. ACM, pp. 57–60, doi:10.1145/1217975.1217986.
  7. 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.
  8. Jared Davis & Sol Swords (2015): XDOC Documentation for FTY. Available at http://www.cs.utexas.edu/users/moore/acl2/manuals/.
  9. Bernard van Gastel & Julien Schmaltz (2013): A formalisation of XMAS. In: ACL2 '13. EPTCS, pp. 111–126, doi:10.4204/EPTCS.114.9.
  10. 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.
  11. David Greve & Matthew Wilding (2003): Typed ACL2 Records. ACL2 '03. Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/greve-wilding_defrecord/defrecord.pdf.
  12. 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.
  13. 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.
  14. Matt Kaufmann & Rob Sumners (2002): Efficient Rewriting of Data Structures in ACL2. ACL2 '02. Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/contrib/kaufmann-sumners/rcd.pdf.
  15. 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.
  16. Anthony P. Morse (1965): A Theory of Sets. Academic Press.
  17. Benjamin Selfridge & Eric Smith (2014): Polymorphic Types in ACL2. In: ACL2 '14. EPTCS, pp. 49–60, doi:10.4204/EPTCS.152.4.
  18. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org