A. Bostan, Algorithmique efficace pour des opérations de base en Calcul formel, 2003.

C. Cohen and T. Coquand, A constructive version of Laplace's proof on the existence of complex roots

C. Cohen and A. Mahboubi, Formal proofs in real algebraic geometry : from ordered fields to quantifier elimination
URL : https://hal.archives-ouvertes.fr/inria-00593738

C. Cohen, Types quotients en coq, Actes des 21ème journées francophones des langages applicatifs, 2010.
DOI : 10.1007/978-3-642-39634-2_17

[. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Lecture Notes in Computer Science, vol.1, issue.258, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11

URL : https://hal.archives-ouvertes.fr/inria-00368403

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Selected papers from the International Workshop on Types for Proofs and Programs, TYPES '00, pp.79-95, 2002.
DOI : 10.1007/3-540-45842-5_6

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, Interactive Theorem Proving, ITP 2011 Proceedings, Lecture Notes in Computer Sciences, 2011.
DOI : 10.1017/S0956796802004501

URL : https://hal.archives-ouvertes.fr/hal-00805966

D. Hilbert, Über die transzendenz der zahlen e und ?, 1893.
DOI : 10.1007/978-3-642-50831-8_1

R. Krebbers and B. Spitters, Computer Certified Efficient Exact Reals in Coq, Conference on Intelligent Computer Mathematics, CICM 2011 Proceedings, Lecture Notes in Artifical Intelligence, 2011.
DOI : 10.1007/978-3-642-04027-6_12

]. S. Lan02 and . Lang, Algebra. Graduate texts in mathematics, 2002.

F. [. Mines, W. Richman, and . Ruitenburg, A course in constructive algebra [Pro] The Mathematical Components Project. SSReflect extension and libraries, Universitext, 1979.