@misc(CoGa:equivalences,
 author       = "John Cowles and Ruben Gamboa",
 year         = "2014",
 title        = "Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis",
 howpublished = "Under review",
)
@phdthesis(Gam:dissertation,
 author       = "R. Gamboa",
 year         = "1999",
 title        = "Mechanically Verifying Real-Valued Algorithms in ACL2",
 school       = "The University of Texas at Austin",
)
@inproceedings(GaCo:chain-rule,
 author       = "R. Gamboa and J. Cowles",
 year         = "2009",
 title        = "The Chain Rule and Friends in {ACL2(r)}",
 booktitle    = "Proceedings of the Eighth International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2009)",
)
@inproceedings(GaCo:inverses,
 author       = "R. Gamboa and J. Cowles",
 year         = "2009",
 title        = "Inverse Functions in {ACL2(r)}",
 booktitle    = "Proceedings of the Eighth International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2009)",
)
@inproceedings(GaCo:cantor-trio,
 author       = "R. Gamboa and J. Cowles",
 year         = "2012",
 title        = "A {C}antor Trio: Denumerability, the Reals, and the Real Algebraic Numbers",
 booktitle    = "Proc of the Third Conference on Interactive Theorem Proving (ITP-2012)",
 doi          = "10.1007/978-3-642-32347-8_5",
)
@incollection(Kau:ftc,
 author       = "M. Kaufmann",
 year         = "2000",
 title        = "Modular Proof: The Fundamental Theorem of Calculus",
 editor       = "M. Kaufmann and P. Manolios and {J S}. Moore",
 booktitle    = "Computer-Aided Reasoning: ACL2 Case Studies",
 chapter      = "6",
 publisher    = "Kluwer Academic Press",
 doi          = "10.1007/978-1-4615-4449-4",
)
@article(Med:arctan,
 author       = "Herbert Medina",
 year         = "2006",
 title        = "A Sequence of Polynomials for Approximating Inverse Tangent",
 journal      = "American Mathematical Monthly",
 volume       = "113",
 number       = "2",
 pages        = "156--161",
 doi          = "10.2307/27641866",
)
@inproceedings(ReGa:automatic-differentiator,
 author       = "P. Reid and R. Gamboa",
 year         = "2011",
 title        = "Automatic Differentiation in ACL2",
 booktitle    = "Proc of the Second Conference on Interactive Theorem Proving (ITP-2011)",
 doi          = "10.1007/978-3-642-22863-6_23",
)
@misc(Rus:transcendentals,
 author       = "David Russinoff",
 year         = "2007",
 title        = "Modeling the Transcendental Instructions with Elementary Polynomial Approximations",
 howpublished = "\url {http://www.russinoff.com/papers/transcendentals.pdf}",
)