Sanaz Khan Afshar, Vincent Aravantinos, Osman Hasan & Sofiène Tahar (2014):
Formalization of Complex Vectors in Higher-Order Logic.
In: Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka & Josef Urban: Intelligent Computer Mathematics.
Springer International Publishing,
Cham,
pp. 123–137,
doi:10.1023/A:1012692601098.
Leif O. Arkeryd, Nigel J. Cutland & C. Ward Henson (Eds.) (1997):
Nonstandard Analysis: Theory and Applications,
1st edition,
Nato Science Series C: 493.
Springer Netherlands,
doi:10.1007/978-94-011-5544-1.
John Cowles & Ruben Gamboa (2017):
The Cayley-Dickson Construction in ACL2.
In: Anna Slobodova & Warren Hunt, Jr.: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017,
Electronic Proceedings in Theoretical Computer Science 249.
Open Publishing Association,
pp. 18–29,
doi:10.4204/EPTCS.249.2.
Ruben A. Gamboa & Matt Kaufmann (2001):
Nonstandard Analysis in ACL2.
Journal of Automated Reasoning 27(4),
pp. 323–351,
doi:10.1023/A:1011908113514.
John Harrison (2005):
A HOL Theory of Euclidean Space.
In: Joe Hurd & Tom Melham: Theorem Proving in Higher Order Logics.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 114–129,
doi:10.1007/11541868_8.
Nathan Jacobson (1985):
Basic Algebra I,
2nd edition.
Dover Publications.
Carl Kwan & Mark R. Greenstreet (2018):
Convex Functions in ACL2(r).
In: Proceedings 15th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, November 5-6, 2018,
this volume of EPTCS.
Open Publishing Association.
Serge Lang (2002):
Algebra,
3rd edition,
Graduate Texts in Mathematics 211.
Springer-Verlag New York,
doi:10.1007/978-1-4613-0041-0.
Peter A. Loeb & Manfred P. H. Wolff (2015):
Nonstandard Analysis for the Working Mathematician,
2nd edition.
Springer Netherlands,
doi:10.1007/978-94-017-7327-0.
Marco Maggesi (2018):
A Formalization of Metric Spaces in HOL Light.
Journal of Automated Reasoning 60(2),
pp. 237–254,
doi:10.1007/s10817-017-9412-x.
Yan Peng & Mark Greenstreet (2015):
Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification.
In: Klaus Havelund, Gerard Holzmann & Rajeev Joshi: NASA Formal Methods.
Springer International Publishing,
Cham,
pp. 310–326,
doi:10.1007/978-3-319-17524-9_22.
Yan Peng & Mark R. Greenstreet (2015):
Extending ACL2 with SMT Solvers.
In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015.,
pp. 61–77,
doi:10.4204/EPTCS.192.6.
Frigyes Riesz & Bela Sz.-Nagy (1990):
Functional Analysis.
Dover Publications.
Abraham Robinson (1966):
Non-Standard Analysis.
North-Holland Publishing Company.
Steven Roman (2008):
Advanced Linear Algebra,
3rd edition,
Graduate Texts in Mathematics 135.
Springer-Verlag New York,
doi:10.1007/978-0-387-72831-5.
Walter Rudin (1976):
Principles of Mathematical Analysis,
3rd edition,
International Series in Pure and Applied Mathematics.
McGraw-Hill.
Georgi E. Shilov (1977):
Linear Algebra.
Dover Publications.
J. Michael Steele (2004):
The Cauchy-Schwarz Master Class: An Introduction to the Art of Mathematical Inequalities.
Cambridge University Press,
doi:10.1017/CBO9780511817106.
Jasper Stein (2001):
Documentation for the formalization of Linerar Agebra.
Online.
Available at http://www.cs.ru.nl/~jasper/.
eptcs@eptcs.org