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