@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},
)
@book(boyd,
 author       = {Stephen Boyd and Lieven Vandenberghe},
 year         = {2004},
 title        = {Convex Optimization},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511804441},
)
@incollection(Gamboa2000,
 author       = {Ruben Gamboa},
 year         = {2000},
 title        = {Continuity and Differentiability},
 editor       = {Matt Kaufmann and Panagiotis Manolios and J. Strother Moore},
 booktitle    = {Computer-Aided Reasoning: ACL2 Case Studies},
 publisher    = {Springer US},
 address      = {Boston, MA},
 pages        = {301--315},
 doi          = {10.1007/978-1-4757-3188-0_18},
)
@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(harrison2007,
 author       = {John Harrison},
 year         = {2007},
 title        = {Formalizing Basic Complex Analysis},
 editor       = {R. Matuszewski and A. Zalewska},
 booktitle    = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
 series       = {Studies in Logic, Grammar and Rhetoric},
 volume       = {10(23)},
 publisher    = {University of Bia{\l}ystok},
 pages        = {151--165},
 url          = {http://mizar.org/trybulec65/},
)
@book(jacob,
 author       = {Nathan Jacobson},
 year         = {1985},
 title        = {Basic Algebra I},
 edition      = {2nd},
 publisher    = {Dover Publications},
)
@incollection(Kaufmann2000,
 author       = {Matt Kaufmann},
 year         = {2000},
 title        = {Modular Proof: The Fundamental Theorem of Calculus},
 editor       = {Matt Kaufmann and Panagiotis Manolios and J. Strother Moore},
 booktitle    = {Computer-Aided Reasoning: ACL2 Case Studies},
 publisher    = {Springer US},
 address      = {Boston, MA},
 pages        = {75--91},
 doi          = {10.1007/978-1-4757-3188-0_6},
)
@conference(Kwan2018-cs,
 author       = {Carl Kwan and Mark R. Greenstreet},
 year         = {2018},
 title        = {Real Vector Spaces and the Cauchy-Schwarz Inequality 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},
)
@book(Nesterov2004,
 author       = {Yurii Nesterov},
 year         = {2004},
 title        = {Introductory Lectures on Convex Optimization},
 edition      = {1st},
 series       = {Applied Optimization 87},
 publisher    = {Springer US},
 doi          = {10.1007/978-1-4419-8853-9},
)
@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},
)