@article(BaBl:nsa,
 author       = "A.M. Ballantyne and W. W. Bledsoe",
 year         = "1977",
 title        = "Automatic Proofs of Theorems in Analysis Using Non-Standard Techniques",
 journal      = "Journal of the Association for Computing Machinery (JACM)",
 volume       = "24",
 number       = "3",
 pages        = "353--371",
 doi          = "10.1145/322017.322018",
)
@phdthesis(Gam:dissertation,
 author       = "R. Gamboa",
 year         = "1999",
 title        = "Mechanically Verifying Real-Valued Algorithms in ACL2",
 school       = "The University of Texas at Austin",
)
@article(GC:acl2r-theory,
 author       = "R. Gamboa and J. Cowles",
 year         = "2007",
 title        = "Theory Extension in {ACL2(r)}",
 journal      = "Journal of Automated Reasoning",
 doi          = "10.1007/s10817-006-9043-0",
)
@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(Nel:nsa,
 author       = "E. Nelson",
 year         = "1977",
 title        = "Internal Set Theory: A New Approach to Nonstandard Analysis",
 journal      = "Bulletin of the American Mathematical Society",
 volume       = "83",
 pages        = "1165--1198",
 doi          = "10.1090/S0002-9904-1977-14398-X",
)
@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",
)
@book(Robinson:nsa,
 author       = "A. Robinson",
 year         = "1996",
 title        = "Non-Standard Analysis",
 publisher    = "Princeton University Press",
)
@book(Rudin:analysis,
 author       = "W. Rudin",
 year         = "1976",
 title        = "Principles of Mathematical Analysis",
 edition      = "third",
 publisher    = "McGraw-Hill",
)
@inproceedings(SaGa:sqrt,
 author       = "J. Sawada and R. Gamboa",
 year         = "2002",
 title        = "Mechanical Verification of a Square Root Algorithm using {T}aylor's Theorem",
 booktitle    = "Formal Methods in Computer-Aided Design (FMCAD'02)",
 doi          = "10.1007/3-540-36126-X_17",
)