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