{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:10:09Z","timestamp":1743084609620,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_18","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"233-248","source":"Crossref","is-referenced-by-count":26,"title":["Formalization of Entropy Measures in HOL"],"prefix":"10.1007","author":[{"given":"Tarek","family":"Mhamdi","sequence":"first","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"Measure Theory","author":"V.I. Bogachev","year":"2006","unstructured":"Bogachev, V.I.: Measure Theory. Springer, Heidelberg (2006)"},{"issue":"1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D. Chaum","year":"1988","unstructured":"Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. Journal of Cryptology\u00a01(1), 65\u201375 (1988)","journal-title":"Journal of Cryptology"},{"key":"18_CR3","unstructured":"Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. PhD thesis, University of Cambridge (2010)"},{"key":"18_CR4","doi-asserted-by":"publisher","DOI":"10.1002\/0471200611","volume-title":"Elements of Information Theory","author":"T.M. Cover","year":"1991","unstructured":"Cover, T.M., Thomas, J.A.: Elements of Information Theory. Wiley Interscience, Hoboken (1991)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-540-75227-1_5","volume-title":"Formal Aspects in Security and Trust","author":"Y. Deng","year":"2007","unstructured":"Deng, Y., Pang, J., Wu, P.: Measuring Anonymity with Relative Entropy. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol.\u00a04691, pp. 65\u201379. Springer, Heidelberg (2007)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-36467-6_5","volume-title":"Privacy Enhancing Technologies","author":"C. D\u00edaz","year":"2003","unstructured":"D\u00edaz, C., Seys, S., Claessens, J., Preneel, B.: Towards Measuring Anonymity. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol.\u00a02482, pp. 54\u201368. Springer, Heidelberg (2003)"},{"key":"18_CR7","volume-title":"Methods of Real Analysis","author":"R.R. Goldberg","year":"1976","unstructured":"Goldberg, R.R.: Methods of Real Analysis. Wiley, Chichester (1976)"},{"key":"18_CR8","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"18_CR9","unstructured":"H\u00f6lzl, J.: Mechanized Measure, Probability, and Information Theory. Technical University Munich, Germany (2010), \n                    \n                      http:\/\/puma.in.tum.de\/p-wiki\/images\/d\/d6\/szentendre_hoelzl_probability.pdf"},{"key":"18_CR10","unstructured":"Hurd, J.: Formal Verifcation of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)"},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2004.01.021","volume":"112","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic Guarded Commands Mechanized in HOL. Electronic Notes in Theoretical Computer Science\u00a0112, 95\u2013111 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/1190215.1190251","volume":"42","author":"P. Malacaria","year":"2007","unstructured":"Malacaria, P.: Assessing Security Threats of Looping Constructs. SIGPLAN Not.\u00a042(1), 225\u2013235 (2007)","journal-title":"SIGPLAN Not."},{"key":"18_CR13","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)"},{"key":"18_CR14","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of Measure and Lebesgue Integration over Extended Reals in HOL. Technical Report, ECE Dept., Concordia University (February 2011), \n                    \n                      http:\/\/hvg.ece.concordia.ca\/Publications\/TECH_REP\/MLX_TR11\/"},{"key":"18_CR15","volume-title":"Probability, Random Variables, and Stochastic Processes","author":"A. Papoulis","year":"1984","unstructured":"Papoulis, A.: Probability, Random Variables, and Stochastic Processes. Mc-Graw Hill, New York (1984)"},{"key":"18_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a Generic Theorem Prover","author":"L. Paulson C.","year":"1994","unstructured":"C. Paulson, L.: Isabelle: a Generic Theorem Prover. Springer, Heidelberg (1994)"},{"issue":"1","key":"18_CR17","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M.K. Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for Web Transactions. ACM Transactions on Information and System Security\u00a01(1), 66\u201392 (1998)","journal-title":"ACM Transactions on Information and System Security"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-36467-6_4","volume-title":"Privacy Enhancing Technologies","author":"A. Serjantov","year":"2003","unstructured":"Serjantov, A., Danezis, G.: Towards an Information Theoretic Metric for Anonymity. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol.\u00a02482, pp. 41\u201353. Springer, Heidelberg (2003)"},{"issue":"3","key":"18_CR19","doi-asserted-by":"publisher","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. The Bell System Technical Journal\u00a027(3), 379\u2013423 (1948)","journal-title":"The Bell System Technical Journal"},{"issue":"23","key":"18_CR20","first-page":"167","volume":"10","author":"Y. Shidama","year":"2007","unstructured":"Shidama, Y., Endou, N., Kawamoto, P.N.: On the formalization of lebesgue integrals. Studies in Logic, Grammar and Rhetoric\u00a010(23), 167\u2013177 (2007)","journal-title":"Studies in Logic, Grammar and Rhetoric"}],"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-22863-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T02:51:39Z","timestamp":1554000699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}