{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:54:38Z","timestamp":1725900878953},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642323461"},{"type":"electronic","value":"9783642323478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_16","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T07:33:54Z","timestamp":1344584034000},"page":"233-249","source":"Crossref","is-referenced-by-count":5,"title":["Formalization of Shannon\u2019s Theorems in SSReflect-Coq"],"prefix":"10.1007","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Manabu","family":"Hagiwara","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1002\/j.1538-7305.1948.tb01338.x","volume":"27","author":"C.E. Shannon","year":"1948","unstructured":"Shannon, C.E.: A Mathematical Theory of Communication. Bell System Technical Journal\u00a027, 379\u2013423, 623\u2013656 (1948)","journal-title":"Bell System Technical Journal"},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"656","DOI":"10.1002\/j.1538-7305.1949.tb00928.x","volume":"28","author":"C.E. Shannon","year":"1949","unstructured":"Shannon, C.E.: Communication Theory of Secrecy Systems. Bell System Technical Journal\u00a028, 656\u2013715 (1949)","journal-title":"Bell System Technical Journal"},{"unstructured":"Uyematsu, T.: Modern Shannon Theory, Information theory with types. Baifukan (1998) (in Japanese)","key":"16_CR3"},{"unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, Trinity College, University of Cambridge, UK (2001)","key":"16_CR4"},{"unstructured":"Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. Wiley-Interscience (2006)","key":"16_CR5"},{"key":"16_CR6","doi-asserted-by":"publisher","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. Reasoning\u00a041, 295\u2013323 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical Big Operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"issue":"8","key":"16_CR8","doi-asserted-by":"publisher","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. Program.\u00a074(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"unstructured":"Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. PhD Thesis, King\u2019s College, University of Cambridge, UK (2010)","key":"16_CR9"},{"unstructured":"The COQ Development Team. Reference Manual. Version 8.3. INRIA (2004-2010), \n                    \n                      http:\/\/coq.inria.fr","key":"16_CR10"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-14052-5_27","volume-title":"Interactive Theorem Proving","author":"T. Mhamdi","year":"2010","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: On the Formalization of the Lebesgue Integration Theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 387\u2013402. Springer, Heidelberg (2010)"},{"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":"16_CR12"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-22863-6_18","volume-title":"Interactive Theorem Proving","author":"T. Mhamdi","year":"2011","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of Entropy Measures in HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 233\u2013248. Springer, Heidelberg (2011)"},{"unstructured":"Affeldt, R., Hagiwara, M.: Formalization of Shannon\u2019s Theorems in SSReflect-COQ. COQ scripts, \n                    \n                      http:\/\/staff.aist.go.jp\/reynald.affeldt\/shannon","key":"16_CR14"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32347-8_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T08:01:04Z","timestamp":1620115264000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}