{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:03Z","timestamp":1740123363885,"version":"3.37.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,1,6]],"date-time":"2020-01-06T00:00:00Z","timestamp":1578268800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,6]],"date-time":"2020-01-06T00:00:00Z","timestamp":1578268800000},"content-version":"vor","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":[[2020,8]]},"DOI":"10.1007\/s10817-019-09538-8","type":"journal-article","created":{"date-parts":[[2020,1,6]],"date-time":"2020-01-06T06:02:31Z","timestamp":1578290551000},"page":"1123-1164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Library for Formalization of Linear Error-Correcting Codes"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2327-953X","authenticated-orcid":false,"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8056-5519","authenticated-orcid":false,"given":"Jacques","family":"Garrigue","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4492-745X","authenticated-orcid":false,"given":"Takafumi","family":"Saikawa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,1,6]]},"reference":[{"key":"9538_CR1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Garrigue, J.: Formalization of error-correcting codes: from Hamming to modern coding theory. In: 6th Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science, vol. 9236, pp. 17\u201333. Springer, Nanjing, China, August 24\u201327 (2015)","DOI":"10.1007\/978-3-319-22102-1_2"},{"issue":"1","key":"9538_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10817-013-9298-1","volume":"53","author":"R Affeldt","year":"2014","unstructured":"Affeldt, R., Hagiwara, M., S\u00e9nizergues, J.: Formalization of Shannon\u2019s theorems. J. Autom. Reason. 53(1), 63\u2013103 (2014)","journal-title":"J. Autom. Reason."},{"key":"9538_CR3","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Formalization of Reed\u2013Solomon codes and progress report on formalization of LDPC codes. In: International Symposium on Information Theory and its Applications (ISITA 2016), pp. 537\u2013541. IEICE, IEEE Xplore, Monterey, California, USA, October 30\u2013November 2 (2016)"},{"key":"9538_CR4","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Reasoning with conditional probabilities and joint distributions in Coq. In: 21st Workshop on Programming and Programming Languages (PPL2019). Japan Society for Software Science and Technology, Iwate-ken, Hanamaki-shi, March 6\u20138 (2019)"},{"key":"9538_CR5","unstructured":"Asai, T.: The SSReflect extension of the Coq proof-assistant and its application. Master\u2019s thesis, Graduate School of Mathematics, Nagoya University (2014). (in Japanese)"},{"issue":"1\u20132","key":"9538_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-1999-391201","volume":"39","author":"C Ballarin","year":"1999","unstructured":"Ballarin, C., Paulson, L.C.: A pragmatic approach to extending provers by computer algebra\u2014with applications to coding theory. Fundam. Inform. 39(1\u20132), 1\u201320 (1999)","journal-title":"Fundam. Inform."},{"issue":"1","key":"9538_CR7","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1016\/S0019-9958(60)90287-4","volume":"3","author":"RC Bose","year":"1960","unstructured":"Bose, R.C., Ray-Chaudhuri, D.K.: On a class of error correcting binary group codes. Inf. Control 3(1), 68\u201379 (1960)","journal-title":"Inf. Control"},{"issue":"6","key":"9538_CR8","doi-asserted-by":"publisher","first-page":"1570","DOI":"10.1109\/TIT.2002.1003839","volume":"48","author":"C Di","year":"2002","unstructured":"Di, C., Proietti, D., Telatar, I.E., Richardson, T.J., Urbanke, R.L.: Finite-length analysis of low-density parity-check codes on the binary erasure channel. IEEE Trans. Inf. Theory 48(6), 1570\u20131579 (2002)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"6","key":"9538_CR9","doi-asserted-by":"publisher","first-page":"2173","DOI":"10.1109\/18.782170","volume":"45","author":"T Etzion","year":"1999","unstructured":"Etzion, T., Trachtenberg, A., Vardy, A.: Which codes have cycle-free Tanner graphs? IEEE Trans. Inf. Theory 45(6), 2173\u20132181 (1999)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"1","key":"9538_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/TIT.1962.1057683","volume":"8","author":"RG Gallager","year":"1962","unstructured":"Gallager, R.G.: Low-density parity-check codes. IRE Trans. Inf. Theory 8(1), 21\u201328 (1962)","journal-title":"IRE Trans. Inf. Theory"},{"key":"9538_CR11","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: 4th International Conference on Interactive Theorem Proving (ITP 2013), pp. 163\u2013179, Rennes, France, July 22\u201326 (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"volume-title":"The Princeton Companion to Mathematics","year":"2008","key":"9538_CR12","unstructured":"Gowers, T. (ed.): The Princeton Companion to Mathematics. Princeton University Press, Princeton (2008)"},{"key":"9538_CR13","volume-title":"Coding Theory: Mathematics for Digital Communication","author":"M Hagiwara","year":"2012","unstructured":"Hagiwara, M.: Coding Theory: Mathematics for Digital Communication. Nippon Hyoron Sha, Toshima (2012). (in Japanese)"},{"key":"9538_CR14","unstructured":"Hagiwara, M., Nakano, K., Kong, J.: Formalization of coding theory using lean. In: International Symposium on Information Theory and Its Applications (ISITA 2016), pp. 527\u2013531. IEICE , IEEE Xplore, Monterey, California, USA, October 30\u2013November 2 (2016)"},{"issue":"2","key":"9538_CR15","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1002\/j.1538-7305.1950.tb00463.x","volume":"XXVI","author":"RW Hamming","year":"1950","unstructured":"Hamming, R.W.: Error detecting and error correcting codes. Bell Syst. Tech. J. XXVI(2), 147\u2013160 (1950)","journal-title":"Bell Syst. Tech. J."},{"key":"9538_CR16","first-page":"147","volume":"2","author":"A Hocquenghem","year":"1959","unstructured":"Hocquenghem, A.: Codes correcteurs d\u2019erreurs. Chiffres (Paris) 2, 147\u2013156 (1959)","journal-title":"Chiffres (Paris)"},{"key":"9538_CR17","unstructured":"Infotheo.: A Coq formalization of information theory and linear error-correcting codes. https:\/\/github.com\/affeldt-aist\/infotheo\/, Coq scripts, version 0.0.2 (2019)"},{"key":"9538_CR18","doi-asserted-by":"crossref","unstructured":"Kong, J., Webb, D.J., Hagiwara, M.: Formalization of insertion\/deletion codes and the Levenshtein metric in lean. In: International Symposium on Information Theory and Its Applications (ISITA 2018), pp .11\u201315. IEICE, IEEE Xplore, Singapore, October 18\u201331 (2018)","DOI":"10.23919\/ISITA.2018.8664354"},{"issue":"2","key":"9538_CR19","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/18.910572","volume":"47","author":"FR Kschischang","year":"2001","unstructured":"Kschischang, F.R., Frey, B.J., Loeliger, H.: Factor graphs and the sum-product algorithm. IEEE Trans. Inf. Theory 47(2), 498\u2013519 (2001)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"9538_CR20","volume-title":"The Theory of Error-Correcting Codes","author":"FJ MacWilliams","year":"1977","unstructured":"MacWilliams, F.J., Sloane, N.J.A.: The Theory of Error-Correcting Codes. Elsevier, New York (1977). (seventh impression 1992)"},{"key":"9538_CR21","unstructured":"Mahboubi, A., Tassi, E.: Mathematical components. Available at: https:\/\/math-comp.github.io\/mcb\/, with contributions by Yves Bertot and Georges Gonthier (2016) Accessed 11 August 2011"},{"key":"9538_CR22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511606267","volume-title":"The Theory of Information and Coding, Encyclopedia of Mathematics and its Applications","author":"RJ McEliece","year":"2002","unstructured":"McEliece, R.J.: The Theory of Information and Coding, Encyclopedia of Mathematics and its Applications, vol. 86. Cambridge University Press, Cambridge (2002)"},{"key":"9538_CR23","unstructured":"Obata, N.: Formalization of theorems about stopping sets and the decoding performance of LDPC codes. Department of Communications and Computer Engineering, Graduate School of Science and Engineering, Tokyo Institute of Technology, Master\u2019s thesis (2015). (in Japanese)"},{"issue":"2","key":"9538_CR24","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1137\/0108018","volume":"8","author":"IS Reed","year":"1960","unstructured":"Reed, I.S., Solomon, G.: Polynomial codes over certain finite fields. J. Soc. Ind. Appl. Math. (SIAM) 8(2), 300\u2013304 (1960)","journal-title":"J. Soc. Ind. Appl. Math. (SIAM)"},{"key":"9538_CR25","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511791338","volume-title":"Modern Coding Theory","author":"T Richardson","year":"2008","unstructured":"Richardson, T., Urbanke, R.: Modern Coding Theory. Cambridge University Press, Cambridge (2008)"},{"issue":"2","key":"9538_CR26","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1109\/18.910577","volume":"47","author":"TJ Richardson","year":"2001","unstructured":"Richardson, T.J., Urbanke, R.L.: The capacity of low-density parity-check codes under message-passing decoding. IEEE Trans. Inf. Theory 47(2), 599\u2013618 (2001)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"1","key":"9538_CR27","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0019-9958(75)90090-X","volume":"27","author":"Y Sugiyama","year":"1975","unstructured":"Sugiyama, Y., Kasahara, M., Hirasawa, S., Namekawa, T.: A method for solving key equation for decoding Goppa codes. Inf. Control 27(1), 87\u201399 (1975)","journal-title":"Inf. Control"},{"key":"9538_CR28","unstructured":"The Coq Development Team.: The Coq proof assistant reference manual. INRIA, version 8.9.0 (2018)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09538-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09538-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09538-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,5]],"date-time":"2021-01-05T00:21:01Z","timestamp":1609806061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09538-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,6]]},"references-count":28,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,8]]}},"alternative-id":["9538"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09538-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,1,6]]},"assertion":[{"value":"25 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 November 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 January 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}