Skip to content

Commit

Permalink
Add papers from ITP 2024. (#537)
Browse files Browse the repository at this point in the history
  • Loading branch information
@grunweg
grunweg authored Oct 10, 2024
1 parent 7bbccea commit f16c3a0
Showing 1 changed file with 212 additions and 2 deletions.
214 changes: 212 additions & 2 deletions lean.bib
View file
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

0 comments on commit f16c3a0

Please sign in to comment.