Interactive Theorem Proving and Program Development , Coq'Art: The Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond ,
DOI : 10.1007/978-3-540-74464-1_4
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
A Small Scale Reflection Extension for the Coq system ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
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
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. ,
Mathematical Components. Draft, 2016. URL https ,
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
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