D. Augot and L. Pecquet, A Hensel Lifting to Replace Factorization in List- Decoding of Algebraic-Geometric and Reed-Solomon Codes. Information Theory, IEEE Transactions on, vol.46, issue.7, pp.2605-2614, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00509339

J. Daniel and . Bernstein, Simplified High-Speed High-Distance List Decoding for Alternant Codes, LNCS, vol.7071, pp.200-216, 2011.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot and G. Gonthier, Sidi Ould Biha, and Ioana Pasca. Canonical Big Operators, pp.86-101

M. Boespflug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, LNCS, vol.7086, pp.362-377, 2011.
DOI : 10.1007/3-540-44464-5_13
URL : https://hal.archives-ouvertes.fr/hal-00650940

D. Boneh, Finding Smooth Integers in Short Intervals Using CRT Decoding, Journal of Computer and System Sciences, vol.64, issue.4, pp.768-784, 2002.
DOI : 10.1006/jcss.2002.1827

N. Brisebarre, M. Jolde?, É. Martin-dorel, M. Mayero, J. Muller et al., Rigorous Polynomial Approximation Using Taylor Models in Coq, NASA Formal Methods 2012, pp.85-99, 2012.
DOI : 10.1007/978-3-642-28891-3_9
URL : https://hal.archives-ouvertes.fr/ensl-00653460

J. Chrz?szcz, Implementing Modules in the Coq System, LNCS, vol.2758, pp.270-286, 2003.
DOI : 10.1007/10930755_18

J. Chrz?szcz, Modules in Coq Are and Will Be Correct, LNCS, vol.3085, pp.130-146, 2003.
DOI : 10.1007/978-3-540-24849-1_9

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for Free!, LNCS, vol.8307, pp.147-162, 2013.
DOI : 10.1007/978-3-319-03545-1_10
URL : https://hal.archives-ouvertes.fr/hal-01113453

D. Coppersmith, Finding a Small Root of a Bivariate Integer Equation; Factoring with High Bits Known, Maurer [28], pp.178-189
DOI : 10.1007/3-540-68339-9_16

D. Coppersmith, Finding a Small Root of a Univariate Modular Equation, Maurer [28], pp.155-165
DOI : 10.1007/3-540-68339-9_14

D. Coppersmith, Small Solutions to Polynomial Equations, and Low Exponent RSA Vulnerabilities, Journal of Cryptology, vol.10, issue.4, pp.233-260, 1997.
DOI : 10.1007/s001459900030

M. Dénès, A. Mörtberg, and V. Siles, A Refinement-Based Approach to Computational Algebra in Coq, LNCS, vol.7406, pp.83-98, 2012.

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

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

V. Guruswami and M. Sudan, Improved decoding of Reed-Solomon and algebraic-geometry codes, IEEE Transactions on Information Theory, vol.45, issue.6, pp.1757-1767, 1999.
DOI : 10.1109/18.782097

F. Haftmann, A. Krauss, O. Kuncar, and T. Nipkow, Data Refinement in Isabelle/HOL, Blazy et al. [5], pp.100-115
DOI : 10.1007/978-3-642-39634-2_10

K. Hensel, Neue Grundlagen der Arithmetik Journal für die reine und angewandte Mathematik (Crelle's Journal), pp.51-84, 1904.

A. Karatsuba and Y. Ofman, Multiplication of Many-Digital Numbers by Automatic Computers . Doklady Akad, Translation in Physics-Doklady, pp.293-294, 1962.

H. Kobayashi, H. Suzuki, and Y. Ono, Formalization of Hensel's lemma, Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, number PRG- RR-05-02 in, pp.114-127, 2005.

P. Lammich, Automatic Data Refinement, Blazy et al. [5], pp.84-99
DOI : 10.1007/978-3-642-39634-2_9

A. K. Lenstra, H. W. Lenstra, J. , and L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen, vol.32, issue.4, pp.515-534, 1982.
DOI : 10.1007/BF01457454

É. Martin, Contributions to the Formal Verification of Arithmetic Algorithms
URL : https://hal.archives-ouvertes.fr/tel-00745553

É. Martin-dorel, M. Mayero, I. Pa?ca, L. Rideau, and L. Théry, Certified, Efficient and Sharp Univariate Taylor Models in COQ, 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp.193-200, 2013.
DOI : 10.1109/SYNASC.2013.33
URL : https://hal.archives-ouvertes.fr/hal-00845791

A. Saïbi, Typing algorithm in type theory with inheritance, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.292-301, 1997.
DOI : 10.1145/263699.263742

M. Sozeau and N. Oury, First-Class Type Classes, pp.278-293
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

D. Stehlé, Algorithmique de la réduction des réseaux et application à la recherche de pires cas pour l'arrondi des fonctions mathématiques

D. Stehlé, On the Randomness of Bits Generated by Sufficiently Smooth Functions, Algorithmic Number Theory, 7th International Symposium, ANTS-VII Proceedings, pp.257-274, 2006.
DOI : 10.1007/11792086_19

D. Stehlé, V. Lefèvre, and P. Zimmermann, Searching worst cases of a one-variable function using lattice reduction, IEEE Transactions on Computers, vol.54, issue.3, pp.340-346, 2005.
DOI : 10.1109/TC.2005.55

G. W. Stewart, On the adjugate matrix, Linear Algebra and its Applications, vol.283, issue.1-3, pp.151-164, 1998.
DOI : 10.1016/S0024-3795(98)10098-8

J. Von, Z. Gathen, and J. Gerhard, Modern Computer Algebra, 2003.