A.M. Ballantyne & W. W. Bledsoe (1977):
Automatic Proofs of Theorems in Analysis Using Non-Standard Techniques.
Journal of the Association for Computing Machinery (JACM) 24(3),
pp. 353–371,
doi:10.1145/322017.322018.
R. Gamboa (1999):
Mechanically Verifying Real-Valued Algorithms in ACL2.
The University of Texas at Austin.
R. Gamboa & J. Cowles (2007):
Theory Extension in ACL2(r).
Journal of Automated Reasoning,
doi:10.1007/s10817-006-9043-0.
M. Kaufmann (2000):
Modular Proof: The Fundamental Theorem of Calculus.
In: M. Kaufmann, P. Manolios & J S. Moore: Computer-Aided Reasoning: ACL2 Case Studies, chapter 6.
Kluwer Academic Press,
doi:10.1007/978-1-4615-4449-4.
E. 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.
P. Reid & R. Gamboa (2011):
Automatic Differentiation in ACL2.
In: Proc of the Second Conference on Interactive Theorem Proving (ITP-2011),
doi:10.1007/978-3-642-22863-6_23.
A. Robinson (1996):
Non-Standard Analysis.
Princeton University Press.
W. Rudin (1976):
Principles of Mathematical Analysis,
third edition.
McGraw-Hill.
J. Sawada & R. Gamboa (2002):
Mechanical Verification of a Square Root Algorithm using Taylor's Theorem.
In: Formal Methods in Computer-Aided Design (FMCAD'02),
doi:10.1007/3-540-36126-X_17.