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