@manual(xdoc,
 author       = {ACL2},
 title        = {A Beginner’s Guide to Reasoning about Quantification in ACL2},
 url          = {https://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____QUANTIFIER-TUTORIAL},
 note         = {Originally written by Sandip Ray},
)
@inproceedings(Afshar,
 author       = {Sanaz Khan Afshar and Vincent Aravantinos and Osman Hasan and Sofi{\`e}ne Tahar},
 year         = {2014},
 title        = {Formalization of Complex Vectors in Higher-Order Logic},
 editor       = {Stephen M. Watt and James H. Davenport and Alan P. Sexton and Petr Sojka and Josef Urban},
 booktitle    = {Intelligent Computer Mathematics},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {123--137},
 doi          = {10.1023/A:1012692601098},
)
@book(cutland,
 author       = {Leif O. Arkeryd and Nigel J. Cutland and C. Ward Henson (Eds.)},
 year         = {1997},
 title        = {Nonstandard Analysis: Theory and Applications},
 edition      = {1st},
 series       = {Nato Science Series C: 493},
 publisher    = {Springer Netherlands},
 doi          = {10.1007/978-94-011-5544-1},
)
@inproceedings(Cowles2017,
 author       = {John Cowles and Ruben Gamboa},
 year         = {2017},
 title        = {The Cayley-Dickson Construction in ACL2},
 editor       = {Anna Slobodova and Warren Hunt, Jr.},
 booktitle    = {{\rm Proceedings 14th International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Austin, Texas, USA, May 22-23, 2017}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {249},
 publisher    = {Open Publishing Association},
 pages        = {18--29},
 doi          = {10.4204/EPTCS.249.2},
)
@article(Gamboa2001,
 author       = {Ruben A. Gamboa and Matt Kaufmann},
 year         = {2001},
 title        = {Nonstandard Analysis in ACL2},
 journal      = {Journal of Automated Reasoning},
 volume       = {27},
 number       = {4},
 pages        = {323--351},
 doi          = {10.1023/A:1011908113514},
)
@inproceedings(Harrison,
 author       = {John Harrison},
 year         = {2005},
 title        = {A HOL Theory of Euclidean Space},
 editor       = {Joe Hurd and Tom Melham},
 booktitle    = {Theorem Proving in Higher Order Logics},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {114--129},
 doi          = {10.1007/11541868_8},
)
@book(jacob,
 author       = {Nathan Jacobson},
 year         = {1985},
 title        = {Basic Algebra I},
 edition      = {2nd},
 publisher    = {Dover Publications},
)
@misc(top100,
 author       = {Nathan Kahl},
 title        = {The Hundred Greatest Theorems},
 howpublished = {Online},
 url          = {http://pirate.shu.edu/~kahlnath/Top100.html},
 note         = {Originally published by Paul and Jack Abad (1999)},
)
@misc(isabelle-cs,
 author       = {Gerwin Klein},
 title        = {The Top 100 Theorems in Isabelle},
 howpublished = {Online},
 url          = {https://www.cse.unsw.edu.au/~kleing/top100/\#78},
)
@conference(Kwan2018-convex,
 author       = {Carl Kwan and Mark R. Greenstreet},
 year         = {2018},
 title        = {Convex Functions in ACL2(r)},
 booktitle    = {{\rm Proceedings 15th International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Austin, Texas, USA, November 5-6, 2018}},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
)
@book(lang,
 author       = {Serge Lang},
 year         = {2002},
 title        = {Algebra},
 edition      = {3rd},
 series       = {Graduate Texts in Mathematics 211},
 publisher    = {Springer-Verlag New York},
 doi          = {10.1007/978-1-4613-0041-0},
)
@book(loeb,
 author       = {Peter A. Loeb and Manfred P. H. Wolff},
 year         = {2015},
 title        = {Nonstandard Analysis for the Working Mathematician},
 edition      = {2nd},
 publisher    = {Springer Netherlands},
 doi          = {10.1007/978-94-017-7327-0},
)
@misc(coq-cs,
 author       = {Jean-Marie Madiot},
 title        = {Formalizing 100 theorems in Coq},
 howpublished = {Online},
 url          = {https://madiot.fr/coq100/\#78},
)
@article(Maggesi2018,
 author       = {Marco Maggesi},
 year         = {2018},
 title        = {A Formalization of Metric Spaces in HOL Light},
 journal      = {Journal of Automated Reasoning},
 volume       = {60},
 number       = {2},
 pages        = {237--254},
 doi          = {10.1007/s10817-017-9412-x},
)
@inproceedings(Peng2015-NASA,
 author       = {Yan Peng and Mark Greenstreet},
 year         = {2015},
 title        = {Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification},
 editor       = {Klaus Havelund and Gerard Holzmann and Rajeev Joshi},
 booktitle    = {NASA Formal Methods},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {310--326},
 doi          = {10.1007/978-3-319-17524-9_22},
)
@inproceedings(Peng2015,
 author       = {Yan Peng and Mark R. Greenstreet},
 year         = {2015},
 title        = {Extending {ACL2} with {SMT} Solvers},
 booktitle    = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015.},
 pages        = {61--77},
 doi          = {10.4204/EPTCS.192.6},
)
@book(riesz,
 author       = {Frigyes Riesz and Sz.-Nagy, Bela},
 year         = {1990},
 title        = {Functional Analysis},
 publisher    = {Dover Publications},
)
@book(robinson,
 author       = {Abraham Robinson},
 year         = {1966},
 title        = {Non-Standard Analysis},
 publisher    = {North-Holland Publishing Company},
)
@book(roman,
 author       = {Steven Roman},
 year         = {2008},
 title        = {Advanced Linear Algebra},
 edition      = {3rd},
 series       = {Graduate Texts in Mathematics 135},
 publisher    = {Springer-Verlag New York},
 doi          = {10.1007/978-0-387-72831-5},
)
@book(babyrudin,
 author       = {Walter Rudin},
 year         = {1976},
 title        = {Principles of Mathematical Analysis},
 edition      = {3rd},
 series       = {International Series in Pure and Applied Mathematics},
 publisher    = {McGraw-Hill},
)
@book(shilov,
 author       = {Georgi E. Shilov},
 year         = {1977},
 title        = {Linear Algebra},
 publisher    = {Dover Publications},
)
@book(steele,
 author       = {J. Michael Steele},
 year         = {2004},
 title        = {The Cauchy-Schwarz Master Class: An Introduction to the Art of Mathematical Inequalities},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511817106},
)
@misc(stein,
 author       = {Jasper Stein},
 year         = {2001},
 title        = {Documentation for the formalization of Linerar Agebra},
 howpublished = {Online},
 url          = {http://www.cs.ru.nl/~jasper/},
)
@misc(top100formal,
 author       = {Freek Wiedijk},
 title        = {Formalizing 100 Theorems},
 howpublished = {Online},
 url          = {http://www.cs.ru.nl/~freek/100},
)
@article(wu2009,
 author       = {Hui-Hua Wu and Shanhe Wu},
 year         = {2009},
 title        = {Various proofs of the Cauchy-Schwarz inequality},
 journal      = {Octogon Mathematical Magazine},
 volume       = {17},
 number       = {1},
 pages        = {221--229},
)