Skip to content

Commit

Permalink
chore: add missing ITP 23 papers (#547)
Browse files Browse the repository at this point in the history 
Includes #546 to avoid merge conflicts. Feel free to rebase, once the
previous one has been merged.
  • Loading branch information
@grunweg
grunweg authored Nov 4, 2024
1 parent bedb9c4 commit 9c4ebbd
Showing 1 changed file with 65 additions and 9 deletions.
74 changes: 65 additions & 9 deletions lean.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -773,6 +777,30 @@ @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}},
Expand Down Expand Up @@ -810,7 +838,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,
Expand Down Expand Up @@ -1152,7 +1181,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,
Expand Down Expand Up @@ -1281,7 +1311,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,
Expand Down Expand Up @@ -1520,7 +1551,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,
Expand Down Expand Up @@ -1649,7 +1681,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,
Expand Down Expand Up @@ -1783,3 +1816,26 @@ @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}
}

0 comments on commit 9c4ebbd

Please sign in to comment.