{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:05Z","timestamp":1750219805914,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575675","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"334-347","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formalization of Doob\u2019s Martingale Convergence Theorems in mathlib"],"prefix":"10.1145","author":[{"given":"Kexing","family":"Ying","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"R\u00e9my","family":"Degenne","sequence":"additional","affiliation":[{"name":"University of Lille, France \/ Inria, France \/ CNRS, France \/ Centrale Lille, France \/ UMR 9198-CRIStAL, France"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Formalization of Shannon\u2019s Theorems in SSReflect-Coq. In 3rd Conference on Interactive Theorem Proving (Lecture Notes in Computer Science","volume":"2012","author":"Affeldt Reynald","year":"2012","unstructured":"Reynald Affeldt and Manabu Hagiwara. 2012. Formalization of Shannon\u2019s Theorems in SSReflect-Coq. In 3rd Conference on Interactive Theorem Proving (Lecture Notes in Computer Science, Vol. 7406). http:\/\/itp2012.cs.princeton.edu\/ Springer, 233\u2013249."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3158456.3158478"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_16"},{"key":"e_1_3_2_1_5_1","unstructured":"Manuel Eberl. 2021. The Laws of Large Numbers. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/Laws_of_Large_Numbers.html"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09528-w"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"S\u00e9bastien Gou\u00ebzel. 2022. A formalization of the change of variables formula for integrals in mathlib. https:\/\/doi.org\/10.48550\/ARXIV.2207.12742","DOI":"10.48550\/ARXIV.2207.12742"},{"key":"e_1_3_2_1_8_1","volume-title":"Mark Veraar, and Lutz Weis.","author":"Hyt\u00f6nen Tuomas","year":"2016","unstructured":"Tuomas Hyt\u00f6nen, Jan Van Neerven, Mark Veraar, and Lutz Weis. 2016. Analysis in Banach spaces. 12, Springer."},{"key":"e_1_3_2_1_9_1","unstructured":"Johannes H\u00f6lzl Andreas Lochbihler and Dmitriy Traytel. 2015. A Zoo of Probabilistic Systems. Archive of Formal Proofs May issn:2150-914x https:\/\/isa-afp.org\/entries\/Probabilistic_System_Zoo.html"},{"key":"e_1_3_2_1_10_1","volume-title":"Foundations of Modern Probability","author":"Kallenberg Olav","unstructured":"Olav Kallenberg. 2021. Foundations of Modern Probability (3rd ed.). Springer.","edition":"3"},{"volume-title":"Bandit algorithms","author":"Lattimore Tor","key":"e_1_3_2_1_11_1","unstructured":"Tor Lattimore and Csaba Szepesv\u00e1ri. 2020. Bandit algorithms. Cambridge University Press."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_14_1","unstructured":"Michael Norrish and Konrad Slind. 2022. The HOL System DESCRIPTION (3 ed.)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5430\/air.v2n4p37"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.31"},{"volume-title":"Probability with martingales","author":"Williams David","key":"e_1_3_2_1_19_1","unstructured":"David Williams. 1991. Probability with martingales. Cambridge university press."}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575675","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575675","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575675"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":19,"alternative-id":["10.1145\/3573105.3575675","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575675","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}