Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
DOI : 10.1007/978-3-540-74464-1_4

F. Chyzak, A. Mahboubi, T. Sibut-pinote, and E. Tassi, A Computer- Algebra-Based Formal Proof of the Irrationality of ?(3), ITP - 5th International Conference on Interactive Theorem Proving
URL : https://hal.archives-ouvertes.fr/hal-00984057

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Theorem Proving in Higher Order Logics (TPHOLs), Proceedings, pp.98-113, 2005.
DOI : 10.1007/11541868_7

N. Magaud, A. Chollet, and L. Fuchs, Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective URL https, Annals of Mathematics and Artificial Intelligence, vol.74, pp.3-4309, 2014.

A. Mahboubi and E. Tassi, Mathematical Components. Draft, 2016. URL https

W. Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing , Supercomputing '91, pp.4-13, 1991.
DOI : 10.1145/125826.125848

T. Zimmermann and H. Herbelin, Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, Conference on Intelligent Computer Mathematics URL, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01152588