{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T17:17:02Z","timestamp":1771262222955,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["GA 742178"],"award-info":[{"award-number":["GA 742178"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003343","name":"Cambridge Trust","doi-asserted-by":"publisher","award":[""],"award-info":[{"award-number":[""]}],"id":[{"id":"10.13039\/501100003343","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636946","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"132-146","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Probabilistic Methods for Combinatorial Structures using the Lov\u00e1sz Local Lemma"],"prefix":"10.1145","author":[{"given":"Chelsea","family":"Edmonds","sequence":"first","affiliation":[{"name":"University of Sheffield, Sheffield, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.3"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.11309\/jssst.37.3_79"},{"key":"e_1_3_2_1_3_1","volume-title":"Spencer","author":"Alon Noga","year":"2016","unstructured":"Noga Alon and Joel H. Spencer. 2016. The Probabilistic Method (4th ed.). Wiley, Hoboken, N.J. isbn:1119061954"},{"key":"e_1_3_2_1_4_1","volume-title":"Contribuciones Cient\u00edficas en Honor de Mirian Andr\u00e9s G\u00f3mez","author":"Ballarin Clemens","unstructured":"Clemens Ballarin. 2010. Tutorial to Locales and Locale Interpretation. In Contribuciones Cient\u00edficas en Honor de Mirian Andr\u00e9s G\u00f3mez. University of Rioja, 123\u2013140. Online at https:\/\/dialnet.unirioja.es\/servlet\/articulo?codigo=3216664"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09537-9"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09612-0"},{"key":"e_1_3_2_1_8_1","volume-title":"Probability & Statistics 1 Coursebook","author":"Chalmers Dean","unstructured":"Dean Chalmers. 2018. Probability & Statistics 1 Coursebook. Cambridge University Press."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.15"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.9"},{"key":"e_1_3_2_1_12_1","unstructured":"Chelsea Edmonds. 2022. Undirected Graph Theory. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Undirected_Graph_Theory.html"},{"key":"e_1_3_2_1_13_1","unstructured":"Chelsea Edmonds. 2023. General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Lovasz_Local.html"},{"key":"e_1_3_2_1_14_1","unstructured":"Chelsea Edmonds. 2023. Hypergraphs. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Hypergraph_Basics.html"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-022-09650-2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81097-9_1"},{"key":"e_1_3_2_1_17_1","volume-title":"Paulson","author":"Edmonds Chelsea","year":"2023","unstructured":"Chelsea Edmonds and Lawrence C. Paulson. 2023. Hypergraph Colouring Bounds. Archive of Formal Proofs, September, issn:2150-914x https:\/\/isa-afp.org\/entries\/Hypergraph_Colourings.html"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.01.001"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9401-5"},{"key":"e_1_3_2_1_21_1","unstructured":"Lars Hupel. 2014. Properties of Random Graphs \u2013 Subgraph Containment. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/Random_Graph_Subgraph_Threshold.html"},{"key":"e_1_3_2_1_22_1","unstructured":"Emin Karayel. 2023. Expander Graphs. Archive of Formal Proofs March https:\/\/isa-afp.org\/entries\/Expander_Graphs.html"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4171\/176-1"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575680"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16681-5_5"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"M. Molloy and B. Reed. 2002. Graph Colouring and the Probabilistic Method. Springer. isbn:978-3-540-42139-9 lccn:2001055101 https:\/\/doi.org\/10.1007\/978-3-642-04016-0 10.1007\/978-3-642-04016-0","DOI":"10.1007\/978-3-642-04016-0"},{"key":"e_1_3_2_1_27_1","unstructured":"Diogo A. C. V. Moreira. 2012. Finite Probability Distributions in Coq. Universidade do Minho. Available at https:\/\/repositorium.sdum.uminho.pt\/bitstream\/1822\/28219\/1\/eeum_di_dissertacao_pg16019.pdf"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_27"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0183-z"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.29007\/36dt"},{"key":"e_1_3_2_1_31_1","first-page":"755","article-title":"Introduction to Probability","volume":"1","author":"Jan Popio\u0142","year":"1990","unstructured":"Jan Popio\u0142 ek. 1990. Introduction to Probability. Formalized Mathematics, 1, 4 (1990), 755\u2013760. http:\/\/fm.mizar.org\/1990-1\/pdf1-4\/rpr_1.pdf","journal-title":"Formalized Mathematics"},{"key":"e_1_3_2_1_32_1","unstructured":"Rishikesh H. Vaishnav. 2022. Formalising the Beginnings of Bayesian Probability Theory in the Lean Theorem Prover. UC San Diego. Available at https:\/\/escholarship.org\/uc\/item\/8hb1w6js"},{"key":"e_1_3_2_1_33_1","volume-title":"Isar - a Versatile Environment for Human Readable Formal Proof Documents","author":"Wenzel Markus","unstructured":"Markus Wenzel. 2002. Isabelle, Isar - a Versatile Environment for Human Readable Formal Proof Documents. Technical University Munich, Germany."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575675"},{"key":"e_1_3_2_1_35_1","volume-title":"Fall","author":"Zhao Yufei","year":"2020","unstructured":"Yufei Zhao. 2020. Probabilistic Methods in Combinatorics. Lecture notes MIT 18.226, Fall 2020, https:\/\/ocw.mit.edu\/courses\/18-226-probabilistic-method-in-combinatorics-fall-2020\/resources\/mit18_226f20_full_notes\/"}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"London UK","acronym":"CPP '24","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636946","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636946","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636946"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":35,"alternative-id":["10.1145\/3636501.3636946","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636946","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}