@article(autarky,
 author       = {Henk Barendregt and Erik Barendsen},
 year         = {2002},
 title        = {Autarchic Computations in Formal Proofs},
 journal      = {Journal of Automated Reasoning},
 volume       = {28},
 pages        = {321--336},
 doi          = {10.1023/A:1015761529444},
)
@inproceedings(bernstein,
 author       = {Daniel J. Bernstein},
 year         = {2006},
 title        = {Curve25519: New Diffie-Hellman Speed Records},
 booktitle    = {9th International Conference on Theory and Practice of Public Key Cryptography},
 publisher    = {Springer},
 pages        = {207--228},
 doi          = {10.1007/11745853_14},
)
@article(bernstein2,
 author       = {Daniel J. Bernstein and Tanja Lange},
 year         = {2011},
 title        = {A Complete Set of Addition Laws for Incomplete Edwards Curves},
 journal      = {Journal of Number Theory},
 volume       = {131},
 pages        = {858--872},
 doi          = {10.1016/j.jnt.2010.06.015},
)
@(friedl,
 author       = {Stefan Friedl},
 year         = {1998},
 title        = {An Elementary Proof of the Group Law for Elliptic Curve},
)
@inproceedings(gregoire,
 author       = {Benjamin Gregoire and Assia Mahboubi},
 year         = {2005},
 title        = {Proving Equalities in a Commutative Ring Done Right in Coq},
 booktitle    = {Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics},
 publisher    = {Springer-Verlag},
 pages        = {98--113},
 doi          = {10.1007/11541868_7},
)
@article(hank,
 author       = {Henri Poincar\'e},
 year         = {1901},
 title        = {Sur les Propri\'et\'es Arithmetiques des Courbes Alg\'ebriques},
 journal      = {Lournalde Math\'ematiques Pures et Appliu\'ees},
 volume       = {7},
 pages        = {121--233},
)
@article(pratt,
 author       = {Vaughn Pratt},
 year         = {1975},
 title        = {Every Prime Has a Succinct Certification},
 journal      = {SIAM Journal on Computing},
 volume       = {4},
 doi          = {10.1137/0204018},
)
@unpublished(shnf,
 author       = {David M. Russinoff},
 title        = {Polynomial Terms and Sparse Horner Normal Form},
 url          = {http://www.russinoff.com/papers/shnf.pdf},
)
@unpublished(prime,
 author       = {David M. Russinoff},
 title        = {Pratt Certification and the Primality of $2^{255}-19$},
 url          = {http://www.russinoff.com/papers/pratt.pdf},
)
@book(tate,
 author       = {Joseph H. Silverman and John T. Tate},
 year         = {2015},
 title        = {Rational Points on Elliptic Curves},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-319-18588-0},
)
@techreport(thery,
 author       = {Laurent Th\'ery},
 year         = {2007},
 title        = {Proving the Group Law for Elliptic Curves Formally},
 type         = {Technical Report},
 number       = {RT-0330},
 institution  = {Inria},
)
@book(tymo,
 author       = {Thomas Tymoczko},
 year         = {1998},
 title        = {Computers and Mathematical Practice: A Case Study},
 publisher    = {Princeton University Press},
)