, Setoids in type theory, Special Issue on Logical Frameworks and Met- alanguages, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972
, Algorithmique efficace pour des opérations de base en Calcul formel, 2003.
, Types quotients en coq Actes des 21ème journées francophones des langages applicatifs, 2010.
, A constructive version of Laplace's proof on the existence of complex roots
, Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Logical Methods in Computer Science, vol.8, issue.1, pp.1-40, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00593738
, A Tactic Language for the System Coq, Lecture Notes in Computer ScienceLNCS)Lecture Notes in Artificial Intelligence (LNAI), vol.1955, pp.85-95, 2000.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070
, 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
, Constructive reals in coq: Axioms and categoricity. In: Selected papers from the International Workshop on Types for Proofs and Programs, TYPES '00, pp.79-95, 2002.
, 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
, Algebra. Graduate texts in mathematics, 2002.
, A course in constructive algebra, Universitext, 1979.
DOI : 10.1007/978-1-4419-8640-5
, Certified exact transcendental real number computation in coq, Theorem Proving in Higher Order Logics, pp.246-261978, 2008.
, SSReflect extension and libraries. http://www.msr-inria. inria