John Cowles & Ruben Gamboa (2014):
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis.
In: Freek Verbeek & Julien Schmaltz: Proceedings of the Twelfth International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2014),
Vienna, Austria,
pp. 89–100,
doi:10.4204/EPTCS.152.8.
William Dunham (1999):
Euler: The Master of Us All.
Mathematical Association of America.
Ruben Gamboa (1999):
Mechanically Verifying Real-Valued Algorithms in ACL2.
University of Texas at Austin.
Edward Nelson (1977):
Internal Set Theory: A New Approach to Nonstandard Analysis.
Bulletin of the American Mathematical Society 83,
pp. 1165–1198,
doi:10.1090/S0002-9904-1977-14398-X.