{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T03:38:15Z","timestamp":1769571495266,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,8,19]],"date-time":"2014-08-19T00:00:00Z","timestamp":1408406400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,1]]},"DOI":"10.1007\/s10817-014-9312-2","type":"journal-article","created":{"date-parts":[[2014,8,18]],"date-time":"2014-08-18T01:46:09Z","timestamp":1408326369000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formally Verified Certificate Checkers for Hardest-to-Round Computation"],"prefix":"10.1007","volume":"54","author":[{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Hanrot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micaela","family":"Mayero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,8,19]]},"reference":[{"issue":"7","key":"9312_CR1","doi-asserted-by":"crossref","first-page":"2605","DOI":"10.1109\/18.887868","volume":"46","author":"D Augot","year":"2000","unstructured":"Augot, D., Pecquet, L.: A Hensel lifting to replace factorization in list-decoding of algebraic-geometric and Reed-Solomon codes. IEEE Trans. Inf. Theory 46(7), 2605\u20132614 (2000)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"9312_CR2","doi-asserted-by":"crossref","unstructured":"Bernstein, D.J.: Simplified high-speed high-distance list decoding for alternant codes. In: Yang, B.-Y. (ed.) PQCrypto, volume 7071 of LNCS, pp. 200\u2013216. Springer (2011)","DOI":"10.1007\/978-3-642-25405-5_13"},{"key":"9312_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer-Verlag (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9312_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal. Proceedings, volume 5170 of LNCS, pp. 86\u2013101. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9312_CR5","doi-asserted-by":"crossref","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M, Gr\u00e9goire, B.: Full Reduction at Full Throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP, volume 7086 of LNCS, pp. 362\u2013377. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_26"},{"issue":"4","key":"9312_CR6","doi-asserted-by":"crossref","first-page":"768","DOI":"10.1006\/jcss.2002.1827","volume":"64","author":"D Boneh","year":"2002","unstructured":"Boneh, D.: Finding smooth integers in short intervals using CRT decoding. J. Comput. Syst. Sci. 64(4), 768\u2013784 (2002)","journal-title":"J. Comput. Syst. Sci."},{"key":"9312_CR7","doi-asserted-by":"crossref","unstructured":"Brisebarre, N., Jolde\u015f, M., Martin-Dorel, \u00c9., Mayero, M., Muller, J.-M., Pa\u015fca, I., Rideau, L., Th\u00e9ry, L.: Rigorous polynomial approximation using Taylor models in Coq. In: Goodloe, A., Person, S. (eds.) NASA Formal Methods 2012, volume 7226 of LNCS, pp. 85\u201399. Springer (2012)","DOI":"10.1007\/978-3-642-28891-3_9"},{"key":"9312_CR8","doi-asserted-by":"crossref","unstructured":"Chrza\u0327szcz, J.: Implementing modules in the Coq system. In: Basin D.A., Wolff, B. (eds.) TPHOLs, volume 2758 of LNCS, pp. 270\u2013286. Springer (2003)","DOI":"10.1007\/10930755_18"},{"key":"9312_CR9","doi-asserted-by":"crossref","unstructured":"Chrza\u0327szcz, J.: Modules in Coq are and will be correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES, volume 3085 of LNCS, pp. 130\u2013146. Springer (2003)","DOI":"10.1007\/978-3-540-24849-1_9"},{"key":"9312_CR10","doi-asserted-by":"crossref","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: Gonthier, G., Norrish, M. (eds.) CPP, volume 8307 of LNCS, pp. 147\u2013162. Springer (2013)","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"9312_CR11","doi-asserted-by":"crossref","unstructured":"Coppersmith, D.: Finding a small root of a bivariate integer equation; factoring with high bits known. In: Maurer, M.U.M. (ed) Advances in Cryptology - EUROCRYPT \u201996, International Conference on the Theory and Application of Cryptographic Techniques, Saragossa. Proceeding, volume 1070 of LNCS, pp. 178\u2013189. Springer (1996)","DOI":"10.1007\/3-540-68339-9_16"},{"key":"9312_CR12","doi-asserted-by":"crossref","unstructured":"Coppersmith, D.: Finding a small root of a univariate modular equation. In: Maurer, M.U.M. (ed.) Advances in Cryptology - EUROCRYPT \u201996, International Conference on the Theory and Application of Cryptographic Techniques, Saragossa. Proceeding, volume 1070 of LNCS, pp. 155\u2013165. Springer (1996)","DOI":"10.1007\/3-540-68339-9_14"},{"issue":"4","key":"9312_CR13","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s001459900030","volume":"10","author":"D Coppersmith","year":"1997","unstructured":"Coppersmith, D.: Small solutions to polynomial equations, and low exponent RSA vulnerabilities. J. Cryptol. 10(4), 233\u2013260 (1997)","journal-title":"J. Cryptol."},{"key":"9312_CR14","unstructured":"The Coq Development Team: The Coq Proof Assistant: Reference Manual: version 8.4pl4, 2014. Available from: http:\/\/coq.inria.fr\/distrib\/current\/refman\/"},{"key":"9312_CR15","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A.P. (eds.) ITP, volume 7406 of LNCS, pp. 83\u201398. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"9312_CR16","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. Research Report RR-6455, INRIA (2008)"},{"issue":"2","key":"9312_CR17","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reason. 3(2), 95\u2013152 (2010)","journal-title":"J. Formalized Reason."},{"issue":"6","key":"9312_CR18","doi-asserted-by":"crossref","first-page":"1757","DOI":"10.1109\/18.782097","volume":"45","author":"V Guruswami","year":"1999","unstructured":"Guruswami, V., Sudan, M.: Improved decoding of Reed-Solomon and algebraic-geometry codes. IEEE Trans. Inf. Theory 45(6), 1757\u20131767 (1999)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"9312_CR19","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Krauss, A., Kuncar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes. Proceedings, volume 7998 of LNCS, pp. 100\u2013115. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_10"},{"issue":"127","key":"9312_CR20","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1515\/crll.1904.127.51","volume":"1904","author":"K Hensel","year":"1904","unstructured":"Hensel, K: Neue Grundlagen der Arithmetik. J. f\u00fcr die reine und angewandte Mathematik (Crelle\u2019s Journal) 1904(127), 51\u201384 (1904). doi: 10.1515\/crll.1904.127.51","journal-title":"J. f\u00fcr die reine und angewandte Mathematik (Crelle\u2019s Journal)"},{"key":"9312_CR21","first-page":"293","volume":"145","author":"A Karatsuba","year":"1963","unstructured":"Karatsuba, A., Ofman, Y.: Multiplication of many-digital numbers by automatic computers. Doklady Akad. Nauk SSSR 145, 293\u2013294 (1963). Translation in Physics-Doklady, 7,595\u2013596","journal-title":"Doklady Akad. Nauk SSSR"},{"key":"9312_CR22","unstructured":"Kobayashi, H., Suzuki, H., Ono, Y.: Formalization of Hensel\u2019s lemma. In: Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, number PRG-RR-05-02 in Oxford University Computing Laboratory Research Reports, pp. 114\u2013127 (2005)"},{"key":"9312_CR23","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes. Proceedings, volume 7998 of LNCS, pp. 84\u201399. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"9312_CR24","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/BF01457454","volume":"261","author":"AK Lenstra","year":"1982","unstructured":"Lenstra, A.K., Lenstra, H.W. Jr., Lov\u00e1sz, L.: Factoring polynomials with rational coefficients. Mathematische Annalen 261, 515\u2013534 (1982)","journal-title":"Mathematische Annalen"},{"key":"9312_CR25","unstructured":"Martin-Dorel, \u00c9.: Contributions to the Formal Verification of Arithmetic Algorithms. PhD thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon, Lyon, France, 2012. Available from: http:\/\/tel.archives-ouvertes.fr\/tel-00745553\/en\/"},{"key":"9312_CR26","doi-asserted-by":"crossref","unstructured":"Martin-Dorel, \u00c9., Mayero, M., Pa\u015fca, I., Rideau, L., Th\u00e9ry, L.: Certified, efficient and sharp univariate taylor models in COQ. In: SYNASC 2013, pp. 193\u2013200. IEEE, Timi\u015foara (2013)","DOI":"10.1109\/SYNASC.2013.33"},{"key":"9312_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"J-M Muller","year":"2010","unstructured":"Muller, J.-M., Brisebarre, N., de Dinechin, F, Jeannerod, C.-P., Lef\u00e8vre, V., Melquiond, G., Revol, N, Stehl\u00e9, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user, Boston (2010)"},{"key":"9312_CR28","doi-asserted-by":"crossref","unstructured":"Sa\u00efbi, A.: Typing algorithm in type theory with inheritance. In: POPL, pp. 292\u2013301 (1997)","DOI":"10.1145\/263699.263742"},{"key":"9312_CR29","doi-asserted-by":"crossref","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal. Proceedings, volume 5170 of LNCS, pp. 278\u2013293. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"9312_CR30","unstructured":"Stehl\u00e9, D.: Algorithmique de la r\u00e9duction des r\u00e9seaux et application \u00e0 la recherche de pires cas pour l\u2019arrondi des fonctions math\u00e9matiques. PhD thesis, Universit\u00e9 Nancy, 1, Henri Poincar\u00e9 (2005)"},{"key":"9312_CR31","doi-asserted-by":"crossref","unstructured":"Stehl\u00e9, D.: On the randomness of bits generated by sufficiently smooth functions. In: Hess, F., Pauli, S., Pohst, M.E. (eds.) Algorithmic Number Theory, 7th International Symposium, ANTS-VII, Berlin. Proceedings, volume 4076 of LNCS, pp. 257\u2013274. Springer (2006)","DOI":"10.1007\/11792086_19"},{"issue":"3","key":"9312_CR32","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1109\/TC.2005.55","volume":"54","author":"D Stehl\u00e9","year":"2005","unstructured":"Stehl\u00e9, D., Lef\u00e8vre, V., Zimmermann, P.: Searching worst cases of a one-variable function using lattice reduction. IEEE Trans. Comput. 54 (3), 340\u2013346 (2005)","journal-title":"IEEE Trans. Comput."},{"key":"9312_CR33","doi-asserted-by":"crossref","unstructured":"Steuding, J.: Diophantine Analysis. Chapman & Hall\/CRC (2005)","DOI":"10.1201\/b15887"},{"issue":"1\u20133","key":"9312_CR34","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/S0024-3795(98)10098-8","volume":"283","author":"GW Stewart","year":"1998","unstructured":"Stewart, G.W.: On the adjugate matrix. Lin. Algebra Appl. 283(1\u20133), 151\u2013164 (1998)","journal-title":"Lin. Algebra Appl."},{"key":"9312_CR35","unstructured":"Joachim von zur, G, Gerhard, J.: Modern Computer Algebra, 2nd edn. Cambridge University Press (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9312-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9312-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9312-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T02:35:29Z","timestamp":1565750129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9312-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,19]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"alternative-id":["9312"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9312-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,19]]}}}