{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T13:57:39Z","timestamp":1773323859284,"version":"3.50.1"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,12,11]],"date-time":"2013-12-11T00:00:00Z","timestamp":1386720000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s10817-013-9298-1","type":"journal-article","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T19:15:14Z","timestamp":1386616514000},"page":"63-103","source":"Crossref","is-referenced-by-count":19,"title":["Formalization of Shannon\u2019s Theorems"],"prefix":"10.1007","volume":"53","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Manabu","family":"Hagiwara","sequence":"additional","affiliation":[]},{"given":"Jonas","family":"S\u00e9nizergues","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,11]]},"reference":[{"key":"9298_CR1","first-page":"233","volume-title":"In: Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 13\u201315, 2012. Lecture Notes in Computer Science, vol. 7406","author":"R Affeldt","year":"2012","unstructured":"Affeldt, R., Hagiwara, M.: Formalization of Shannon\u2019s Theorems in SSReflect-Coq. In: Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 13\u201315, 2012. Lecture Notes in Computer Science, vol. 7406, pp. 233\u2013249. Springer, Heidelberg (2012)"},{"key":"9298_CR2","unstructured":"Affeldt, R., Hagiwara, M., S\u00e9nizergues, J.: Formalization of Shannon\u2019s Theorems in SSReflect-Coq. Coq documentation and scripts available at http:\/\/staff.aist.go.jp\/reynald.affeldt\/shannon"},{"issue":"8","key":"9298_CR3","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Prog. 74(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Prog."},{"key":"9298_CR4","first-page":"11","volume-title":"Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 2012. Lecture Notes in Computer Science, vol. 7406,","author":"G Barthe","year":"2012","unstructured":"Barthe, G., Crespo, J.M., Gr\u00e9goire, B., Kunz, C., Zanella B\u00e9guelin, S.: Computer-Aided Cryptographic Proofs. In: Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 2012. Lecture Notes in Computer Science, vol. 7406, pp. 11\u201327. Springer, Heidelberg (2012)"},{"key":"9298_CR5","first-page":"86","volume-title":"Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Montreal, Canada, August 18\u201321, 2008. Lecture Notes in Computer Science, vol. 5170","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical Big Operators. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Montreal, Canada, August 18\u201321, 2008. Lecture Notes in Computer Science, vol. 5170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"9298_CR6","volume-title":"Anonymity, Information, and Machine-Assisted Proof. PhD Thesis, King\u2019s College","author":"AR Coble","year":"2010","unstructured":"Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. PhD Thesis, King\u2019s College. University of Cambridge, UK (2010)"},{"key":"9298_CR7","unstructured":"The Coq Development Team. Reference Manual. Version 8.4. Available at http:\/\/coq.inria.fr . INRIA (2004\u20132012)"},{"key":"9298_CR8","unstructured":"Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. Wiley-Interscience (2006)"},{"issue":"6","key":"9298_CR9","doi-asserted-by":"crossref","first-page":"2505","DOI":"10.1109\/18.720546","volume":"44","author":"I Csisz\u00e1r","year":"1998","unstructured":"Csisz\u00e1r, I.: The method of types. IEEE Trans. Inform. Theory 44(6), 2505\u20132523 (1998)","journal-title":"IEEE Trans. Inform. Theory"},{"key":"9298_CR10","doi-asserted-by":"crossref","unstructured":"Csisz\u00e1r, I., K\u00f6rner, J.: Information Theory\u2014Coding Theorems for Discrete Memoryless Systems, 2nd edn. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511921889"},{"key":"9298_CR11","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Version 10. Technical Report RR-6455, INRIA (2011)"},{"key":"9298_CR12","unstructured":"Hagiwara, M.: Coding Theory: Mathematics for Digital Communication. In Japanese. http:\/\/www.nippyo.co.jp\/book\/5977.html . Nippon Hyoron Sha (2012)"},{"key":"9298_CR13","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s10817-008-9113-6","volume":"41","author":"O Hasan","year":"2008","unstructured":"Hasan, O., Tahar, S.: Verification of expectation using theorem proving to verify expectation and variance for discrete random variables. J. Autom. Reason. 41, 295\u2013323 (2008)","journal-title":"J. Autom. Reason."},{"key":"9298_CR14","first-page":"135","volume-title":"Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 22\u201325, 2011. Lecture Notes in Computer Science, vol. 6898","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three Chapters of Measure Theory in Isabelle\/HOL. In: Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 22\u201325, 2011. Lecture Notes in Computer Science, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011)"},{"key":"9298_CR15","volume-title":"Formal Verification of Probabilistic Algorithms. PhD Thesis, Trinity College","author":"J Hurd","year":"2001","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, Trinity College, University of Cambridge, UK (2001)"},{"key":"9298_CR16","first-page":"387","volume-title":"Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, July 11\u201314, 2010. Lecture Notes in Computer Science, vol. 6172","author":"T Mhamdi","year":"2010","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: On the Formalization of the Lebesgue Integration Theory in HOL. In: Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, July 11\u201314, 2010. Lecture Notes in Computer Science, vol. 6172, pp. 387\u2013402. Springer, Heidelberg (2010)"},{"key":"9298_CR17","first-page":"233","volume-title":"Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 22\u201325, 2011. Lecture Notes in Computer Science, vol. 6898","author":"T Mhamdi","year":"2010","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of Entropy Measures in HOL. In: Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 22\u201325, 2011. Lecture Notes in Computer Science, vol. 6898, pp. 233\u2013248. Springer, Heidelberg (2011)"},{"key":"9298_CR18","unstructured":"Khudanpur, S.: Information Theoretic Methods in Statistics. Lecture Notes. Available at http:\/\/old-site.clsp.jhu.edu\/sanjeev\/520.674\/notes\/GISAlgorithm.pdf (1999). Accessed 02 May 2013"},{"key":"9298_CR19","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1002\/j.1538-7305.1948.tb01338.x","volume":"27","author":"CE Shannon","year":"1948","unstructured":"Shannon, C.E.: A Mathematical theory of communication. Bell Syst. Tech. J. 27, 379\u2013423 and 623\u2013656 (1948)","journal-title":"Bell Syst. Tech. J"},{"key":"9298_CR20","doi-asserted-by":"crossref","first-page":"656","DOI":"10.1002\/j.1538-7305.1949.tb00928.x","volume":"28","author":"CE Shannon","year":"1949","unstructured":"Shannon, C.E.: Communication theory of secrecy systems. Bell Sys. Tech. J. 28, 656\u2013715 (1949)","journal-title":"Bell Sys. Tech. J"},{"key":"9298_CR21","unstructured":"Uyematsu, T.: Modern Shannon Theory, Information Theory with Types. In Japanese. Baifukan (1998)"},{"issue":"6","key":"9298_CR22","doi-asserted-by":"crossref","first-page":"2057","DOI":"10.1109\/18.720531","volume":"44","author":"S Verd\u00fa","year":"1998","unstructured":"Verd\u00fa, S.: Fifty years of Shannon theory. IEEE Trans. Inform. Theory 44(6), 2057\u20132078 (1998)","journal-title":"IEEE Trans. Inform. Theory"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9298-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9298-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9298-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:52Z","timestamp":1559251312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9298-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,11]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["9298"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9298-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,11]]}}}