A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL

Angeliki Koutsoukou-Argyraki; Mantas Bakšys; Chelsea Edmonds

doi:10.1145/3573105.3575680

A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL

Angeliki Koutsoukou-Argyraki, Mantas Bakšys, Chelsea Edmonds

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Original language	English
Title of host publication	CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023
Editors	Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
Publisher	Association for Computing Machinery, Inc
Pages	225-238
Number of pages	14
ISBN (Electronic)	9798400700262
DOIs	https://doi.org/10.1145/3573105.3575680
Publication status	Published - 11 Jan 2023
Event	12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023 - Boston, United States Duration: 16 Jan 2023 → 17 Jan 2023

Conference

Conference	12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023
Country/Territory	United States
City	Boston
Period	16/01/23 → 17/01/23

Keywords

additive combinatorics
formalisation of mathematics
graph theory
interactive theorem proving
Isabelle/HOL
probabilistic method
proof assistant

Access to Document

10.1145/3573105.3575680Licence: CC BY-NC

Cite this

Koutsoukou-Argyraki, A., Bakšys, M., & Edmonds, C. (2023). A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. In R. Krebbers, D. Traytel, B. Pientka, & S. Zdancewic (Eds.), CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023 (pp. 225-238). Association for Computing Machinery, Inc. https://doi.org/10.1145/3573105.3575680

Koutsoukou-Argyraki, Angeliki ; Bakšys, Mantas ; Edmonds, Chelsea. / A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023. editor / Robbert Krebbers ; Dmitriy Traytel ; Brigitte Pientka ; Steve Zdancewic. Association for Computing Machinery, Inc, 2023. pp. 225-238

@inproceedings{f9779d49a5ca404d8723e9f5f536471e,

title = "A Formalisation of the Balog-Szemer{\'e}di-Gowers Theorem in Isabelle/HOL",

keywords = "additive combinatorics, formalisation of mathematics, graph theory, interactive theorem proving, Isabelle/HOL, probabilistic method, proof assistant",

author = "Angeliki Koutsoukou-Argyraki and Mantas Bak{\v s}ys and Chelsea Edmonds",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.; 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023 ; Conference date: 16-01-2023 Through 17-01-2023",

year = "2023",

month = jan,

day = "11",

doi = "10.1145/3573105.3575680",

language = "English",

pages = "225--238",

editor = "Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic",

booktitle = "CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023",

publisher = "Association for Computing Machinery, Inc",

}

Koutsoukou-Argyraki, A, Bakšys, M & Edmonds, C 2023, A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. in R Krebbers, D Traytel, B Pientka & S Zdancewic (eds), CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023. Association for Computing Machinery, Inc, pp. 225-238, 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023, Boston, United States, 16/01/23. https://doi.org/10.1145/3573105.3575680

A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. / Koutsoukou-Argyraki, Angeliki; Bakšys, Mantas; Edmonds, Chelsea.
CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023. ed. / Robbert Krebbers; Dmitriy Traytel; Brigitte Pientka; Steve Zdancewic. Association for Computing Machinery, Inc, 2023. p. 225-238.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL

AU - Koutsoukou-Argyraki, Angeliki

AU - Bakšys, Mantas

AU - Edmonds, Chelsea

PY - 2023/1/11

Y1 - 2023/1/11

KW - additive combinatorics

KW - formalisation of mathematics

KW - graph theory

KW - interactive theorem proving

KW - Isabelle/HOL

KW - probabilistic method

KW - proof assistant

UR - http://www.scopus.com/inward/record.url?scp=85147012936&partnerID=8YFLogxK

U2 - 10.1145/3573105.3575680

DO - 10.1145/3573105.3575680

M3 - Conference contribution

AN - SCOPUS:85147012936

SP - 225

EP - 238

BT - CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023

A2 - Krebbers, Robbert

A2 - Traytel, Dmitriy

A2 - Pientka, Brigitte

A2 - Zdancewic, Steve

PB - Association for Computing Machinery, Inc

T2 - 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023

Y2 - 16 January 2023 through 17 January 2023

ER -

Koutsoukou-Argyraki A, Bakšys M, Edmonds C. A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. In Krebbers R, Traytel D, Pientka B, Zdancewic S, editors, CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023. Association for Computing Machinery, Inc. 2023. p. 225-238 doi: 10.1145/3573105.3575680

A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL

Conference

Keywords

Access to Document

Other files and links

Cite this