S. Basu, R. Pollack, and M. Roy, Algorithms in real algebraic geometry, volume 10 of Algorithms and Computation in Mathematics, 2003.

S. Boulmé, Vers la spécification formelle d'un algorithme non trivial de calcul formel : le calcul de pgcd de deux polynômes par la cha??necha??ne de pseudo-restes de sous-résultants, 1997.

W. S. Brown and J. F. Traub, On Euclid's Algorithm and the Theory of Subresultants, Journal of the ACM, vol.18, issue.4, pp.505-514, 1971.
DOI : 10.1145/321662.321665

G. E. Collins, Subresultants and Reduced Polynomial Remainder Sequences, Journal of the ACM, vol.14, issue.1, pp.128-142, 1967.
DOI : 10.1145/321371.321381
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.8488

D. Delahaye and M. Mayero, Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System, Proceedings of Calculemus 2005, 2005.
DOI : 10.1016/j.entcs.2005.11.023
URL : https://hal.archives-ouvertes.fr/hal-01125075

V. C. Barthe and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972

K. Geddes, S. R. Czapor, and G. Labahn, Algorithms for computer algebra, 1992.
DOI : 10.1007/b102438

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, International Conference on Functional Programming 2002, pp.235-246, 2002.

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLs'2005
DOI : 10.1007/11541868_7

J. Harrison and L. Théry, A skeptic's approach to combining HOL and Maple, Journal of Automated Reasoning, vol.21, issue.3, pp.279-294, 1998.
DOI : 10.1023/A:1006023127567

C. Jacobi, De eliminatione variablilis e duabus aequationibus, J. Reine Angew. Math, p.1836
DOI : 10.1017/cbo9781139567978.011

D. Knuth, The Art of Computer Programming, Semi-numerical algorithmms, 1998.

H. Liao and R. J. Fateman, Evaluation of the heuristic polynomial GCD, Proceedings of the 1995 international symposium on Symbolic and algebraic computation , ISSAC '95, pp.240-247, 1995.
DOI : 10.1145/220346.220376

A. Mahboubi, Programming and certifying a cad algorithm in the coq system, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings. IBFI, Schloss Dagstuhl, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00819492

C. Sacerdoti, A semi-reflexive tactic for (sub-)equational reasoning, Lecture Notes in Computer Sciences, vol.3839, pp.98-114, 2004.

L. Théry, A machine-checked implementation of buchberger's algorithm, Journal of Automated Reasoning, vol.26, issue.2, pp.107-137, 2001.
DOI : 10.1023/A:1026518331905

J. Zur-gathen and T. Lücking, Subresultants revisited, Theoretical Computer Science, issue.297, pp.199-239, 2003.

C. K. Yap, Fundamental Problems of Algorithmic Algebra, 2000.