@misc(abcl,
 title        = {Armed Bear Common Lisp ({ABCL})},
 howpublished = {\url{https://abcl.org}},
)
@misc(acl2-manual,
 title        = {{ACL2} Theorem Prover and Community Books: User Manual},
 howpublished = {\url{http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual}},
)
@misc(apt,
 title        = {{APT} ({Automated Program Transformations})},
 howpublished = {\url{http://www.kestrel.edu/home/projects/apt}},
)
@misc(cffi,
 title        = {{CFFI}: The Common Foreign Function Interface},
 howpublished = {\url{https://common-lisp.net/project/cffi}},
)
@inproceedings(abnf,
 author       = {Alessandro Coglio},
 year         = {2018},
 title        = {A Formalization of the {ABNF} Notation and a Verified Parser of {ABNF} Grammars},
 booktitle    = {Proc.\ 10th Working Conference on Verified Software: Theories, Tools, and Experiments ({VSTTE})},
 note         = {To appear in Springer LNCS},
)
@inproceedings(simplify,
 author       = {Alessandro Coglio and Matt Kaufmann and Eric Smith},
 year         = {2017},
 title        = {A Versatile, Sound Tool for Simplifying Definitions},
 booktitle    = {Proc.\ 14th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2017})},
 pages        = {61--77},
 doi          = {10.4204/EPTCS.249.5},
)
@misc(coq-refman,
 title        = {Coq 8.8.1 Reference Manual},
 howpublished = {\url{https://coq.inria.fr}},
)
@misc(isa-codegen,
 author       = {{Florian Haftmann with contributions from Lukas Bulwahn}},
 year         = {2017},
 title        = {Code generation from Isabelle/HOL theories},
 howpublished = {\url{https://isabelle.in.tum.de}},
 note         = {Tutorial distributed with Isabelle/HOL},
)
@misc(jni,
 title        = {Java Native Interface {JNI} Specification},
 howpublished = {\url{https://docs.oracle.com/javase/10/docs/specs/jni}},
)
@book(parteval,
 author       = {Neil D. Jones and Carsten K. Gomard and Peter Sestoft},
 year         = {1999},
 title        = {Partial Evaluation and Automatic Program Generation},
 publisher    = {Prentice Hall},
 note         = {\url{http://www.itu.dk/people/sestoft/pebook}},
)
@techreport(acl2-logic,
 author       = {Matt Kaufmann and J Strother Moore},
 year         = {1998},
 title        = {A Precise Description of the {ACL2} Logic},
 type         = {Technical Report},
 institution  = {Department of Computer Sciences, University of Texas at Austin},
 note         = {\url{http://www.cs.utexas.edu/users/moore/publications/km97a.pdf}},
)
@article(lisp,
 author       = {John McCarthy},
 year         = {1960},
 title        = {Recursive Functions of Symbolic Expressions and Their Computation by Machine, {Part I}},
 journal      = {Communications of the {ACM}},
 volume       = {3},
 number       = {4},
 pages        = {184--195},
 doi          = {10.1145/367177.367199},
)
@inproceedings(pvs-codegen,
 author       = {Nararajan Shankar},
 year         = {2017},
 title        = {A Brief Introduction to the {PVS2C} Code Generator},
 booktitle    = {Proc.\ Workshop on Automated Formal Methods ({AFM'17})},
)
@book(cltl2,
 author       = {Guy L. Steele},
 year         = {1990},
 title        = {{Common Lisp} the Language},
 publisher    = {Digital Press},
 note         = {\url{https://www.cs.cmu.edu/Groups/AI/html/cltl/cltl2.html}},
)