Andrew W. Appel (1998):
SSA is Functional Programming.
In: SIGPLAN Notices 33.
ACM,
pp. 17–20.
Robert S. Boyer & J Strother Moore (2002):
Single-Threaded Objects in ACL2.
PADL 2002,
doi:10.1007/3-540-45587-6_3.
The Coq Development Team (2013):
The Coq Proof Assistant Reference Manual.
Version 8.4pl21.
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.
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/.
David Greve & Matthew Wilding (2003):
Typed ACL2 Records.
In: ACL2 Workshop 2003.
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.
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.
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.
Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers,
doi:10.1007/978-1-4757-3188-0.
Xavier Leroy (2009):
Formal Verification of a Realistic Compiler.
In: Communications of the ACM 52,
pp. 107–115,
doi:10.1145/1538788.1538814.
LispWorks Ltd.:
Common Lisp HyperSpec.
http://www.lispworks.com/documentation/HyperSpec/Front/index.htm.
LLVM Project:
The LLVM Compiler Infrastructure.
http://llvm.org/.
Magnus O. Myreen, Michael J. C. Gordon & Konrad L. Slind (2012):
Decompilation into Logic — Improved.
In: FMCAD'12.
ACM/IEEE.
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.