References

  1. Andrew W. Appel (1998): SSA is Functional Programming. In: SIGPLAN Notices 33. ACM, pp. 17–20.
  2. Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. PADL 2002, doi:10.1007/3-540-45587-6_3.
  3. The Coq Development Team (2013): The Coq Proof Assistant Reference Manual. Version 8.4pl21.
  4. Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman & F. Kenneth Zadeck (1991): Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. In: TOPLAS 13. ACM, pp. 451–490, doi:10.1145/115372.115320.
  5. Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Remy & Jerome Vouillon: The OCaml System Release 4.00 Documentation and Users Guide. http://caml.inria.fr/pub/docs/manual-ocaml/.
  6. David Greve & Matthew Wilding (2003): Typed ACL2 Records. In: ACL2 Workshop 2003.
  7. David A. Greve (2009): Assuming Termination. In: S. Ray & D. Russinoff: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications. ACM, pp. 114–122, doi:10.1145/1637837.1637856.
  8. David A. Greve & Konrad L. Slind (2013): A Step-Indexing Approach to Partial Functions. In: R. Gamboa & J. Davis: Proceedings of the 11th International Workshop on the ACL2 Theorem Prover and its Applications 114. EPTCS, pp. 42–53, doi:10.4204/EPTCS.114.4.
  9. David S. Hardin, Jedidiah R. McClurg & Jennifer A. Davis (2013): Creating Formally Verified Components for Layered Assurance with an LLVM-to-ACL2 Translator. In: Proceedings of the 2013 Layered Assurance Workshop. ACM.
  10. Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, doi:10.1007/978-1-4757-3188-0.
  11. Xavier Leroy (2009): Formal Verification of a Realistic Compiler. In: Communications of the ACM 52, pp. 107–115, doi:10.1145/1538788.1538814.
  12. LispWorks Ltd.: Common Lisp HyperSpec. http://www.lispworks.com/documentation/HyperSpec/Front/index.htm.
  13. LLVM Project: The LLVM Compiler Infrastructure. http://llvm.org/.
  14. Panagiotis Manolios (2012): Reasoning About Programs. Technical Report. Northeastern University. Available at http://www.ccs.neu.edu/course/cs2800f12/01-acl2s.pdf.
  15. Magnus O. Myreen, Michael J. C. Gordon & Konrad L. Slind (2012): Decompilation into Logic — Improved. In: FMCAD'12. ACM/IEEE.
  16. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin & Steve Zdancewic (2012): Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In: POPL'12. ACM, doi:10.1145/2103621.2103709.

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