Robert S Boyer, David M Goldschlag, Matt Kaufmann & J Strother Moore (1991):
Functional instantiation in first order logic.
In: GROUP, UNIVERSITY OF GOTEBORG.
Citeseer,
pp. 7–26,
doi:10.1016/B978-0-12-450010-5.50007-4.
C. Eastlund & M. Felleisen (2011):
Hygienic macros for ACL2.
Trends in Functional Programming,
pp. 84–101,
doi:10.1007/978-3-642-22941-1_6.
Carl Eastlund & Matthias Felleisen (2009):
Making induction manifest in modular ACL2.
In: Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming.
ACM,
pp. 105–116,
doi:10.1145/1599410.1599424.
R. Gamboa & M. Patterson (2003):
Polymorphism in ACL2.
In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications.
M. Kaufmann & J.S. Moore (2011):
How Can I Do That with ACL2? Recent Enhancements to ACL2.
In: Tenth International Workshop on the ACL2 Theorem Prover and Its Applications 70,
doi:10.4204/EPTCS.70.4.
L. Lambán, F.J. Martín-Mateos, J. Rubio & J.L. Ruiz-Reina (2012):
Formalization of a normalization theorem in simplicial topology.
Annals of Mathematics and Artificial Intelligence 64(1),
pp. 1–37,
doi:10.1007/s10472-011-9274-6.
F. J. Martín-Mateos, J. A. Alonso, M. J. Hidalgo & J. L. Ruiz-Reina (2002):
A generic instantiation tool and a case study: A generic multiset theory.
In: Third International Workshop on the ACL2 Theorem Prover and Its Applications,
pp. 188–203.
J S. Moore (2009):
Automatically computing functional instantiations.
In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications.
ACM,
pp. 11–19,
doi:10.1145/1637837.1637839.
S. Ray & M. Kaufmann (2006):
Defspec.lisp.
ACL2 books/make-event directory.
Freek Verbeek & Julien Schmaltz (2012):
Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures.
ACM Transactions on Design Automation of Electronic Systems 17(1),
doi:10.1145/2071356.2071357.