John Cowles & Ruben Gamboa (2014):
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis.
Under review.
R. Gamboa (1999):
Mechanically Verifying Real-Valued Algorithms in ACL2.
The University of Texas at Austin.
R. Gamboa & J. Cowles (2009):
The Chain Rule and Friends in ACL2(r).
In: Proceedings of the Eighth International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2009).
R. Gamboa & J. Cowles (2009):
Inverse Functions in ACL2(r).
In: Proceedings of the Eighth International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2009).
R. Gamboa & J. Cowles (2012):
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers.
In: Proc of the Third Conference on Interactive Theorem Proving (ITP-2012),
doi:10.1007/978-3-642-32347-8_5.
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.
Herbert Medina (2006):
A Sequence of Polynomials for Approximating Inverse Tangent.
American Mathematical Monthly 113(2),
pp. 156–161,
doi:10.2307/27641866.
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.
David Russinoff (2007):
Modeling the Transcendental Instructions with Elementary Polynomial Approximations.
http://www.russinoff.com/papers/transcendentals.pdf.
eptcs@eptcs.org