{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T01:12:25Z","timestamp":1725844345510},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_27","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"387-402","source":"Crossref","is-referenced-by-count":44,"title":["On the Formalization of the Lebesgue Integration Theory 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":"27_CR1","volume-title":"Fundamentals of Real Analysis.","author":"S.K. Berberian","year":"1998","unstructured":"Berberian, S.K.: Fundamentals of Real Analysis. Springer, Heidelberg (1998)"},{"key":"27_CR2","volume-title":"Measure Theory","author":"V.I. Bogachev","year":"2006","unstructured":"Bogachev, V.I.: Measure Theory. Springer, Heidelberg (2006)"},{"unstructured":"Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. PhD thesis, University of Cambridge, UK (2009)","key":"27_CR3"},{"key":"27_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":"27_CR5","volume-title":"Methods of Real Analysis","author":"R.R. Goldberg","year":"1976","unstructured":"Goldberg, R.R.: Methods of Real Analysis. Wiley, Chichester (1976)"},{"issue":"9","key":"27_CR6","doi-asserted-by":"publisher","first-page":"493","DOI":"10.2307\/2304332","volume":"51","author":"P.R. Halmos","year":"1944","unstructured":"Halmos, P.R.: The foundations of probability. The American Mathematical Monthly\u00a051(9), 493\u2013510 (1944)","journal-title":"The American Mathematical Monthly"},{"key":"27_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL Theory of Euclidean Space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"issue":"4","key":"27_CR9","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1002\/mma.1055","volume":"32","author":"A. Hasan","year":"2009","unstructured":"Hasan, A., Tahar, S.: Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical Methods in the Applied Sciences\u00a032(4), 480\u2013504 (2009)","journal-title":"Mathematical Methods in the Applied Sciences"},{"unstructured":"Hurd, J.: Formal Verifcation of Probabilistic Algorithms. PhD thesis, University of Cambridge, UK (2002)","key":"27_CR10"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1345169.1345171","volume-title":"workshop on Automated Formal Methods","author":"D. Lester","year":"2007","unstructured":"Lester, D.: Topology in PVS: Continuous Mathematics with Applications. In: workshop on Automated Formal Methods, pp. 11\u201320. ACM, New York (2007)"},{"doi-asserted-by":"crossref","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of the Lebesgue Integration Theory in HOL. Technical Report, ECE Dept., Concordia University (April 2009), http:\/\/hvg.ece.concordia.ca\/Publications\/TECH_REP\/MLP_TR10\/","key":"27_CR12","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"27_CR13","volume-title":"Topology","author":"J. Munkres","year":"1999","unstructured":"Munkres, J.: Topology. Prentice Hall, Englewood Cliffs (1999)"},{"key":"27_CR14","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":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-540-30142-4_20","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Richter","year":"2004","unstructured":"Richter, S.: Formalizing Integration Theory with an Application to Probabilistic Algorithms. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 271\u2013286. Springer, Heidelberg (2004)"}],"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-14052-5_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T08:35:16Z","timestamp":1635669316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}