From 817963a2a38e510512190b9180cb34af79d29bb3 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 2 Nov 2024 13:51:37 +0100 Subject: [PATCH 1/3] chore: add tags to all ITP24 papers I verified that all are using Lean 4. I am reasonably confident that 'formalization' is a reasonable categorisation of them all; I'm happy to change the tag for the *duper* paper. --- lean.bib | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/lean.bib b/lean.bib index 5534adb93..52ccc0aac 100644 --- a/lean.bib +++ b/lean.bib @@ -71,7 +71,8 @@ @InProceedings{ Asgeirsson24 urn = {urn:nbn:de:0030-drops-207347}, doi = {10.4230/LIPIcs.ITP.2024.6}, annote = {Keywords: Condensed mathematics, N\"{o}beling’s theorem, - Lean, Mathlib, Interactive theorem proving} + Lean, Mathlib, Interactive theorem proving}, + tags = {formalization, lean4} } @Book{ Avig14, @@ -236,7 +237,8 @@ @InProceedings{ BasoldBruinLawson24 urn = {urn:nbn:de:0030-drops-207368}, doi = {10.4230/LIPIcs.ITP.2024.8}, annote = {Keywords: Lean, Directed Topology, Van Kampen Theorem, - Directed Homotopy Theory, Formalised Mathematics} + Directed Homotopy Theory, Formalised Mathematics}, + tags = {formalization, lean4} } @Booklet{ Best2021, @@ -292,7 +294,8 @@ @InProceedings{ BhatKeizerHughesGoensGrosser24 urn = {urn:nbn:de:0030-drops-207372}, doi = {10.4230/LIPIcs.ITP.2024.9}, annote = {Keywords: compilers, semantics, mechanization, MLIR, SSA, - regions, peephole rewrites} + regions, peephole rewrites}, + tags = {formalization, lean4} } @Article{ BordgCavalleri2021, @@ -443,7 +446,8 @@ @InProceedings{ CluneQianBentkampAvigad24 urn = {urn:nbn:de:0030-drops-207381}, doi = {10.4230/LIPIcs.ITP.2024.10}, annote = {Keywords: proof search, automatic theorem proving, - interactive theorem proving, Lean, dependent type theory} + interactive theorem proving, Lean, dependent type theory}, + tags = {formalization, lean4} } @InProceedings{ CommelinLewis21, @@ -810,7 +814,8 @@ @InProceedings{ Ezeh24 urn = {urn:nbn:de:0030-drops-207690}, doi = {10.4230/LIPIcs.ITP.2024.41}, annote = {Keywords: Interactive theorem proving, Lean4, Graphical - User Interface} + User Interface}, + tags = {formalization, lean4} } @Misc{ FernandezMir19, @@ -1152,7 +1157,8 @@ @InProceedings{ Massot24 urn = {urn:nbn:de:0030-drops-207550}, doi = {10.4230/LIPIcs.ITP.2024.27}, annote = {Keywords: mathematics teaching, proof assistant, - controlled natural language} + controlled natural language}, + tags = {formalization, lean4} } @InProceedings{ Mathlib, @@ -1281,7 +1287,8 @@ @InProceedings{ ObendraufBaanenKoopmanStebletsova24 doi = {10.4230/LIPIcs.ITP.2024.28}, annote = {Keywords: Multi-agent systems, Coalition Logic, Epistemic Logic, common knowledge, completeness, formal methods, Lean - prover} + prover}, + tags = {formalization, lean4} } @Article{ PNWT22, @@ -1520,7 +1527,8 @@ @InProceedings{ SubercaseauxNawrockiGallicchioCodelCarneiroHeule24 urn = {urn:nbn:de:0030-drops-207633}, doi = {10.4230/LIPIcs.ITP.2024.35}, annote = {Keywords: Empty Hexagon Number, Discrete Computational - Geometry, Erd\H{o}s-Szekeres} + Geometry, Erd\H{o}s-Szekeres}, + tags = {formalization, lean4} } @InProceedings{ TassarottiVBT21, @@ -1649,7 +1657,8 @@ @InProceedings{ vanDoornMacbeth24 urn = {urn:nbn:de:0030-drops-207657}, doi = {10.4230/LIPIcs.ITP.2024.37}, annote = {Keywords: Sobolev inequality, measure theory, Lean, - formalized mathematics} + formalized mathematics}, + tags = {formalization, lean4} } @Misc{ VonRaumer15, From 8b08db245efd05705b7c669d4ed19c6ae6a32c9d Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 2 Nov 2024 14:08:32 +0100 Subject: [PATCH 2/3] chore: add missing ITP 23 papers --- lean.bib | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/lean.bib b/lean.bib index 52ccc0aac..952a03b9f 100644 --- a/lean.bib +++ b/lean.bib @@ -777,6 +777,26 @@ @Article{ DupuisLewisMacbeth22 tags = {formalization, lean3} } +@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15, + author = {Dvorak, Martin and Blanchette, Jasmin}, + title = {{Closure Properties of General Grammars – Formally Verified}}, + booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, + pages = {15:1--15:16}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-284-6}, + ISSN = {1868-8969}, + year = {2023}, + volume = {268}, + editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15}, + URN = {urn:nbn:de:0030-drops-183906}, + doi = {10.4230/LIPIcs.ITP.2023.15}, + annote = {Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}, + tags = {formalization, lean3} +} + @Article{ EURAM17, author = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo {de Moura}}, @@ -1792,3 +1812,23 @@ @InProceedings{ YingDegenne23 bibsource = {dblp computer science bibliography, https://dblp.org}, tags = {formalization, lean3} } + +@InProceedings{Zhang23, + author = {Zhang, Jujian}, + title = {{Formalising the Proj Construction in Lean}}, + booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, + pages = {35:1--35:17}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-284-6}, + ISSN = {1868-8969}, + year = {2023}, + volume = {268}, + editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35}, + URN = {urn:nbn:de:0030-drops-184105}, + doi = {10.4230/LIPIcs.ITP.2023.35}, + annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry}, + tags = {formalization, lean3} +} \ No newline at end of file From f4e42136bac88afccfe3e810011dfe1825ea4ceb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 2 Nov 2024 14:10:44 +0100 Subject: [PATCH 3/3] Normalise. --- lean.bib | 77 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 42 insertions(+), 35 deletions(-) diff --git a/lean.bib b/lean.bib index 952a03b9f..43ea9da84 100644 --- a/lean.bib +++ b/lean.bib @@ -777,23 +777,27 @@ @Article{ DupuisLewisMacbeth22 tags = {formalization, lean3} } -@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15, - author = {Dvorak, Martin and Blanchette, Jasmin}, - title = {{Closure Properties of General Grammars – Formally Verified}}, - booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, - pages = {15:1--15:16}, - series = {Leibniz International Proceedings in Informatics (LIPIcs)}, - ISBN = {978-3-95977-284-6}, - ISSN = {1868-8969}, - year = {2023}, - volume = {268}, - editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, - publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, - address = {Dagstuhl, Germany}, - URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15}, - URN = {urn:nbn:de:0030-drops-183906}, - doi = {10.4230/LIPIcs.ITP.2023.15}, - annote = {Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}, +@InProceedings{ dvorak_et_al:LIPIcs.ITP.2023.15, + author = {Dvorak, Martin and Blanchette, Jasmin}, + title = {{Closure Properties of General Grammars – Formally + Verified}}, + booktitle = {14th International Conference on Interactive Theorem + Proving (ITP 2023)}, + pages = {15:1--15:16}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + isbn = {978-3-95977-284-6}, + issn = {1868-8969}, + year = {2023}, + volume = {268}, + editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15}, + urn = {urn:nbn:de:0030-drops-183906}, + doi = {10.4230/LIPIcs.ITP.2023.15}, + annote = {Keywords: Lean, type-0 grammars, recursively enumerable + languages, Kleene star}, tags = {formalization, lean3} } @@ -1813,22 +1817,25 @@ @InProceedings{ YingDegenne23 tags = {formalization, lean3} } -@InProceedings{Zhang23, - author = {Zhang, Jujian}, - title = {{Formalising the Proj Construction in Lean}}, - booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, - pages = {35:1--35:17}, - series = {Leibniz International Proceedings in Informatics (LIPIcs)}, - ISBN = {978-3-95977-284-6}, - ISSN = {1868-8969}, - year = {2023}, - volume = {268}, - editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, - publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, - address = {Dagstuhl, Germany}, - URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35}, - URN = {urn:nbn:de:0030-drops-184105}, - doi = {10.4230/LIPIcs.ITP.2023.35}, - annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry}, +@InProceedings{ Zhang23, + author = {Zhang, Jujian}, + title = {{Formalising the Proj Construction in Lean}}, + booktitle = {14th International Conference on Interactive Theorem + Proving (ITP 2023)}, + pages = {35:1--35:17}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + isbn = {978-3-95977-284-6}, + issn = {1868-8969}, + year = {2023}, + volume = {268}, + editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35}, + urn = {urn:nbn:de:0030-drops-184105}, + doi = {10.4230/LIPIcs.ITP.2023.35}, + annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, + Proj construction, projective geometry}, tags = {formalization, lean3} -} \ No newline at end of file +}