{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:07Z","timestamp":1750219807083,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"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:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"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"}]},{"name":"Cambridge Mathematics Placements Programme","award":[""],"award-info":[{"award-number":[""]}]},{"name":"University of Cambridge Department of Computer Science and Technology","award":[""],"award-info":[{"award-number":[""]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575680","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"225-238","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Formalisation of the Balog\u2013Szemer\u00e9di\u2013Gowers Theorem in Isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Angeliki","family":"Koutsoukou-Argyraki","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mantas","family":"Bak\u0161ys","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chelsea","family":"Edmonds","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_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_2_1","unstructured":"Mantas Bak\u0161ys and Angeliki Koutsoukou-Argyraki. 2022. Kneser\u2019s Theorem and the Cauchy\u2013Davenport Theorem. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Kneser_Cauchy_Davenport.html"},{"volume-title":"Contribuciones Cient\u00edficas en Honor de Mirian Andr\u00e9s G\u00f3mez","author":"Ballarin Clemens","key":"e_1_3_2_1_3_1","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_4_1","unstructured":"Clemens Ballarin. 2019. A Case Study in Basic Algebra. Archive of Formal Proofs August issn:2150-914x https:\/\/isa-afp.org\/entries\/Jacobson_Basic_Algebra.html"},{"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.1007\/BF01212974"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2022.2062073"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.15"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.9"},{"key":"e_1_3_2_1_10_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_11_1","volume-title":"Paulson","author":"Edmonds Chelsea","year":"2021","unstructured":"Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. 2021. Roth\u2019s Theorem on Arithmetic Progressions. Archive of Formal Proofs, December, issn:2150-914x https:\/\/isa-afp.org\/entries\/Roth_Arithmetic_Progressions.html"},{"key":"e_1_3_2_1_12_1","volume-title":"Paulson","author":"Edmonds Chelsea","year":"2021","unstructured":"Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. 2021. Szemer\u00e9di\u2019s Regularity Lemma. Archive of Formal Proofs, November, issn:2150-914x https:\/\/isa-afp.org\/entries\/Szemeredi_Regularity.html"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2207.07499"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81097-9_1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2017.185.1.8"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00039-001-0332-9"},{"key":"e_1_3_2_1_17_1","unstructured":"William Timothy Gowers. 2022. Introduction to Additive Combinatorics. Lecture notes for Part III of the Mathematics Tripos taught at the University of Cambridge available at https:\/\/drive.google.com\/file\/d\/1ut0mUqSyPMweoxoDTfhXverEONyFgcuO\/view"},{"key":"e_1_3_2_1_18_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_19_1","unstructured":"Angeliki Koutsoukou-Argyraki Mantas Bak\u0161ys and Chelsea Edmonds. 2022. The Balog\u2013Szemer\u00e9di\u2013Gowers Theorem. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Balog_Szemeredi_Gowers.html"},{"key":"e_1_3_2_1_20_1","volume-title":"Paulson","author":"Koutsoukou-Argyraki Angeliki","year":"2022","unstructured":"Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. 2022. Khovanskii\u2019s Theorem. Archive of Formal Proofs, September, issn:2150-914x https:\/\/isa-afp.org\/entries\/Khovanskii_Theorem.html"},{"key":"e_1_3_2_1_21_1","volume-title":"Paulson","author":"Koutsoukou-Argyraki Angeliki","year":"2022","unstructured":"Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. 2022. The Pl\u00fcnnecke-Ruzsa Inequality. Archive of Formal Proofs, May, issn:2150-914x https:\/\/isa-afp.org\/entries\/Pluennecke_Ruzsa_Inequality.html"},{"key":"e_1_3_2_1_22_1","unstructured":"Katharina Kreuzer and Manuel Eberl. 2021. Van der Waerden\u2019s Theorem. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Van_der_Waerden.html"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16681-5_5"},{"volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","key":"e_1_3_2_1_24_1","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer. Online at http:\/\/isabelle.in.tum.de\/dist\/Isabelle\/doc\/tutorial.pdf"},{"key":"e_1_3_2_1_25_1","unstructured":"Benedikt Nordhoff and Peter Lammich. 2012. Dijkstra\u2019s Shortest Path Algorithm. Archive of Formal Proofs January issn:2150-914x https:\/\/isa-afp.org\/entries\/Dijkstra_Shortest_Path.html"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Lars Noschinski. 2012. A Probabilistic Proof of the Girth-Chromatic Number Theorem. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/Girth_Chromatic.html","DOI":"10.1007\/978-3-642-32347-8_27"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_27"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0183-z"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(86)90015-4"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.29007\/36dt"},{"key":"e_1_3_2_1_32_1","volume-title":"Combinatorics (Proc. Fifth Hungarian Colloq.","author":"Ruzsa Imre Z.","year":"1978","unstructured":"Imre Z. Ruzsa. 1978. On the cardinality of A+A and A-A. In Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976). 2, 933\u2013938."},{"volume-title":"Sumsets and structure. Lecture notes","author":"Ruzsa Imre Z.","key":"e_1_3_2_1_33_1","unstructured":"Imre Z. Ruzsa. 2008. Sumsets and structure. Lecture notes, Institute of Mathematics, Budapest, available at https:\/\/www.math.cmu.edu\/users\/af1p\/Teaching\/AdditiveCombinatorics\/Additive-Combinatorics.pdf"},{"volume-title":"5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France. http:\/\/aitp-conference.org\/2020\/abstract\/paper_9.pdf Informal proceedings","author":"Stathopoulos Yiannos","key":"e_1_3_2_1_34_1","unstructured":"Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. 2020. Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges. In 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France. http:\/\/aitp-conference.org\/2020\/abstract\/paper_9.pdf Informal proceedings"},{"key":"e_1_3_2_1_35_1","volume-title":"Paulson","author":"Stathopoulos Yiannos","year":"2020","unstructured":"Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. 2020. SErAPIS: A Concept-Oriented Search Engine for the Isabelle Libraries Based on Natural Language. In Isabelle Workshop 2020 (in virtual space). https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_4.pdf Informal proceedings"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1215\/S0012-7094-04-12915-X"},{"key":"e_1_3_2_1_37_1","unstructured":"Ujkan Sulejmani Manuel Eberl and Katharina Kreuzer. 2022. The Hales\u2013Jewett Theorem. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Hales_Jewett.html"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511755149"},{"key":"e_1_3_2_1_39_1","unstructured":"Ren\u00e9 Thiemann. 2021. The Sunflower Lemma of Erd\u0151s and Rado. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/Sunflowers.html"},{"volume-title":"Isar - a Versatile Environment for Human Readable Formal Proof Documents","author":"Wenzel Markus","key":"e_1_3_2_1_40_1","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_41_1","doi-asserted-by":"crossref","unstructured":"Yufei Zhao. 2022. Graph Theory and Additive Combinatorics. Online at. https:\/\/yufeizhao.com\/gtacbook\/ book draft","DOI":"10.1017\/9781009310956"}],"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.3575680","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575680","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.3575680"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":41,"alternative-id":["10.1145\/3573105.3575680","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575680","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"}}]}}