Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 4:1-4:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{baanen:LIPIcs.ITP.2022.4, author = {Baanen, Anne}, title = {{Use and Abuse of Instance Parameters in the Lean Mathematical Library}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {4:1--4:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4}, URN = {urn:nbn:de:0030-drops-167131}, doi = {10.4230/LIPIcs.ITP.2022.4}, annote = {Keywords: formalization of mathematics, dependent type theory, typeclasses, algebraic hierarchy, Lean prover} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Emin Karayel. Formalization of Randomized Approximation Algorithms for Frequency Moments. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 21:1-21:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{karayel:LIPIcs.ITP.2022.21, author = {Karayel, Emin}, title = {{Formalization of Randomized Approximation Algorithms for Frequency Moments}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {21:1--21:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.21}, URN = {urn:nbn:de:0030-drops-167308}, doi = {10.4230/LIPIcs.ITP.2022.21}, annote = {Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Štěpán Holub and Štěpán Starosta. Formalization of Basic Combinatorics on Words. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 22:1-22:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{holub_et_al:LIPIcs.ITP.2021.22, author = {Holub, \v{S}t\v{e}p\'{a}n and Starosta, \v{S}t\v{e}p\'{a}n}, title = {{Formalization of Basic Combinatorics on Words}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {22:1--22:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.22}, URN = {urn:nbn:de:0030-drops-139177}, doi = {10.4230/LIPIcs.ITP.2021.22}, annote = {Keywords: combinatorics on words, formalization, Isabelle/HOL} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Julian Brunner, Benedikt Seidl, and Salomon Sickert. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 11:1-11:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{brunner_et_al:LIPIcs.ITP.2019.11, author = {Brunner, Julian and Seidl, Benedikt and Sickert, Salomon}, title = {{A Verified and Compositional Translation of LTL to Deterministic Rabin Automata}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.11}, URN = {urn:nbn:de:0030-drops-110664}, doi = {10.4230/LIPIcs.ITP.2019.11}, annote = {Keywords: Automata Theory, Automata over Infinite Words, Deterministic Automata, Linear Temporal Logic, Model Checking, Verified Algorithms} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 15:1-15:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{dahmen_et_al:LIPIcs.ITP.2019.15, author = {Dahmen, Sander R. and H\"{o}lzl, Johannes and Lewis, Robert Y.}, title = {{Formalizing the Solution to the Cap Set Problem}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {15:1--15:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.15}, URN = {urn:nbn:de:0030-drops-110703}, doi = {10.4230/LIPIcs.ITP.2019.15}, annote = {Keywords: formal proof, combinatorics, cap set problem, Lean} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 16:1-16:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{eberl:LIPIcs.ITP.2019.16, author = {Eberl, Manuel}, title = {{Nine Chapters of Analytic Number Theory in Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {16:1--16:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.16}, URN = {urn:nbn:de:0030-drops-110714}, doi = {10.4230/LIPIcs.ITP.2019.16}, annote = {Keywords: Isabelle, theorem proving, analytic number theory, number theory, arithmetical function, Dirichlet series, prime number theorem, Dirichlet’s theorem, zeta function, L functions} }
Feedback for Dagstuhl Publishing