Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: add papers from ITP 2024 #537

Merged
merged 1 commit into from
Oct 10, 2024
Merged

chore: add papers from ITP 2024 #537

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
214 changes: 212 additions & 2 deletions lean.bib
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@

# To normalize:
# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i lean.bib -o lean.bib
@InProceedings{ AGLST23,
author = {Avigad, Jeremy and Goldberg, Lior and Levit, David and
Seginer, Yoav and Titelman, Alon},
Expand Down Expand Up @@ -49,6 +47,31 @@ @InProceedings{ AngdinataXu23
tags = {formalization, lean3}
}

# To normalize:
# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i lean.bib -o lean.bib
@InProceedings{ Asgeirsson24,
author = {Asgeirsson, Dagur},
title = {{Towards Solid Abelian Groups: A Formal Proof of
N\"{o}beling’s Theorem}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.6},
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}
}

@Book{ Avig14,
author = "Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho",
title = {{Theorem Proving in Lean}},
Expand Down Expand Up @@ -192,6 +215,28 @@ @Article{ BaanenDahmenNarayananNuccio22
tags = {formalization, lean3}
}

@InProceedings{ BasoldBruinLawson24,
author = {Basold, Henning and Bruin, Peter and Lawson, Dominique},
title = {{The Directed Van Kampen Theorem in Lean}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8},
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}
}

@Booklet{ Best2021,
author = {Alexander Best},
title = {Automatically Generalizing Theorems Using Typeclasses},
Expand Down Expand Up @@ -225,6 +270,29 @@ @InProceedings{ BestBirkbeckBrascaRodriguez23
tags = {formalization, lean3}
}

@InProceedings{ BhatKeizerHughesGoensGrosser24,
author = {Bhat, Siddharth and Keizer, Alex and Hughes, Chris and
Goens, Andr\'{e}s and Grosser, Tobias},
title = {{Verifying Peephole Rewriting in SSA Compiler IRs}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.9},
urn = {urn:nbn:de:0030-drops-207372},
doi = {10.4230/LIPIcs.ITP.2024.9},
annote = {Keywords: compilers, semantics, mechanization, MLIR, SSA,
regions, peephole rewrites}
}

@Article{ BordgCavalleri2021,
author = {Anthony Bordg and Nicol{\`{o}} Cavalleri},
title = {Elements of Differential Geometry in Lean: {A} Report for
Expand Down Expand Up @@ -352,6 +420,30 @@ @InProceedings{ Clune23
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{ CluneQianBentkampAvigad24,
author = {Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander
and Avigad, Jeremy},
title = {{Duper: A Proof-Producing Superposition Theorem Prover for
Dependent Type Theory}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10},
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}
}

@InProceedings{ CommelinLewis21,
author = {Commelin, Johan and Lewis, Robert Y.},
title = {Formalizing the Ring of Witt Vectors},
Expand Down Expand Up @@ -696,6 +788,29 @@ @Article{ EURAM17
tags = {about-lean, lean3}
}

@InProceedings{ Ezeh24,
author = {Ezeh, Sam},
title = {{Graphical Rewriting for Diagrammatic Reasoning in
Monoidal Categories in Lean4}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {41:1--41:8},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41},
urn = {urn:nbn:de:0030-drops-207690},
doi = {10.4230/LIPIcs.ITP.2024.41},
annote = {Keywords: Interactive theorem proving, Lean4, Graphical
User Interface}
}

@Misc{ FernandezMir19,
author = {Ramon Fernández Mir},
title = {Schemes in Lean},
Expand Down Expand Up @@ -1015,6 +1130,29 @@ @Article{ Madelaine19
tags = {about-mathlib, lean3}
}

@InProceedings{ Massot24,
author = {Massot, Patrick},
title = {{Teaching Mathematics Using Lean and Controlled Natural
Language}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {27:1--27:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.27},
urn = {urn:nbn:de:0030-drops-207550},
doi = {10.4230/LIPIcs.ITP.2024.27},
annote = {Keywords: mathematics teaching, proof assistant,
controlled natural language}
}

@InProceedings{ Mathlib,
title = {The {L}ean mathematical library},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International
Expand Down Expand Up @@ -1119,6 +1257,31 @@ @InProceedings{ NawrockiAyersEbner23
tags = {about-lean, lean4}
}

@InProceedings{ ObendraufBaanenKoopmanStebletsova24,
author = {Obendrauf, Kai and Baanen, Anne and Koopmann, Patrick and
Stebletsova, Vera},
title = {{Lean Formalization of Completeness Proof for Coalition
Logic with Common Knowledge}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.28},
urn = {urn:nbn:de:0030-drops-207560},
doi = {10.4230/LIPIcs.ITP.2024.28},
annote = {Keywords: Multi-agent systems, Coalition Logic, Epistemic
Logic, common knowledge, completeness, formal methods, Lean
prover}
}

@Article{ PNWT22,
author = {Porncharoenwase, Sorawee and Nelson, Luke and Wang, Xi and
Torlak, Emina},
Expand Down Expand Up @@ -1334,6 +1497,30 @@ @Misc{ StricklandBellumat19
tags = {formalization, lean3}
}

@InProceedings{ SubercaseauxNawrockiGallicchioCodelCarneiroHeule24,
author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and
Gallicchio, James and Codel, Cayden and Carneiro, Mario and
Heule, Marijn J. H.},
title = {{Formal Verification of the Empty Hexagon Number}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {35:1--35:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35},
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}
}

@InProceedings{ TassarottiVBT21,
author = {Tassarotti, Joseph and Vajjha, Koundinya and Banerjee,
Anindya and Tristan, Jean-Baptiste},
Expand Down Expand Up @@ -1440,6 +1627,29 @@ @InProceedings{ VanDoornEbnerLewis20
tags = {about-mathlib, lean3}
}

@InProceedings{ vanDoornMacbeth24,
author = {van Doorn, Floris and Macbeth, Heather},
title = {{Integrals Within Integrals: A Formalization of the
Gagliardo-Nirenberg-Sobolev Inequality}},
booktitle = {15th International Conference on Interactive Theorem
Proving (ITP 2024)},
pages = {37:1--37:18},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-95977-337-9},
issn = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37},
urn = {urn:nbn:de:0030-drops-207657},
doi = {10.4230/LIPIcs.ITP.2024.37},
annote = {Keywords: Sobolev inequality, measure theory, Lean,
formalized mathematics}
}

@Misc{ VonRaumer15,
author = {Jakob {von Raumer}},
title = {Formalization of Non-Abelian Topology for Homotopy Type
Expand Down
Loading