{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T01:40:26Z","timestamp":1768009226545,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642228629","type":"print"},{"value":"9783642228636","type":"electronic"}],"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_12","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"135-151","source":"Crossref","is-referenced-by-count":50,"title":["Three Chapters of Measure Theory in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Johannes","family":"H\u00f6lzl","sequence":"first","affiliation":[]},{"given":"Armin","family":"Heller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Bauer, H.: Measure and Integration theory. de Gruyter (2001)","DOI":"10.1515\/9783110866209"},{"key":"12_CR2","unstructured":"Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. Ph.D. thesis, King\u2019s College, University of Cambridge (2009)"},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"167","DOI":"10.2478\/v10037-008-0023-1","volume":"16","author":"N. Endou","year":"2008","unstructured":"Endou, N., Narita, K., Shidama, Y.: The Lebesgue monotone convergence theorem. Formal Mathematics\u00a016(2), 167\u2013175 (2008)","journal-title":"Formal Mathematics"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-02444-3_10","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2009","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 153\u2013168. Springer, Heidelberg (2009)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J.V. Harrison","year":"2005","unstructured":"Harrison, J.V.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"12_CR6","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis. University of Cambridge (2002)"},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science\u00a0346(1), 96\u2013112 (2005)","journal-title":"Theoretical Computer Science"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Lester, D.R.: Topology in PVS: continuous mathematics with applications. In: Proceedings of AFM 2007, pp. 11\u201320 (2007)","DOI":"10.1145\/1345169.1345171"},{"key":"12_CR9","unstructured":"Merkl, F.: Dynkin\u2019s lemma in measure theory. In: FM, vol.\u00a09(3), pp. 591\u2013595 (2001)"},{"key":"12_CR10","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":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"12_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810886","volume-title":"Measures, Integrals and Martingales","author":"R.L. Schilling","year":"2005","unstructured":"Schilling, R.L.: Measures, Integrals and Martingales. Cambridge Univ. Press, Cambridge (2005)"}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:13:42Z","timestamp":1560449622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}