LIPIcs, Volume 268
ITP 2023, July 31 to August 4, 2023, Białystok, Poland
Editors: Adam Naumowicz and René Thiemann
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Dagur Asgeirsson. Towards Solid Abelian Groups: A Formal Proof of Nöbeling’s Theorem. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{asgeirsson:LIPIcs.ITP.2024.6, 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} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{clune_et_al:LIPIcs.ITP.2024.10, 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} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12, author = {Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie}, title = {{A Modular Formalization of Superposition in Isabelle/HOL}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {12:1--12: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.12}, URN = {urn:nbn:de:0030-drops-207401}, doi = {10.4230/LIPIcs.ITP.2024.12}, annote = {Keywords: Superposition, verification, first-order logic, higher-order logic} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ekici_et_al:LIPIcs.ITP.2024.13, author = {Ekici, Burak and Yoshida, Nobuko}, title = {{Completeness of Asynchronous Session Tree Subtyping in Coq}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {13:1--13: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.13}, URN = {urn:nbn:de:0030-drops-207418}, doi = {10.4230/LIPIcs.ITP.2024.13}, annote = {Keywords: asynchronous multiparty session types, session trees, subtyping, Coq} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Michikazu Hirata. A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{hirata:LIPIcs.ITP.2024.21, author = {Hirata, Michikazu}, title = {{A Formalization of the L\'{e}vy-Prokhorov Metric in Isabelle/HOL}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {21:1--21: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.21}, URN = {urn:nbn:de:0030-drops-207492}, doi = {10.4230/LIPIcs.ITP.2024.21}, annote = {Keywords: formalization of mathematics, measure theory, metric spaces, topology, L\'{e}vy-Prokhorov metric, Prokhorov’s theorem, Isabelle/HOL} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Dohan Kim. An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kim:LIPIcs.ITP.2024.24, author = {Kim, Dohan}, title = {{An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {24:1--24: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.24}, URN = {urn:nbn:de:0030-drops-207525}, doi = {10.4230/LIPIcs.ITP.2024.24}, annote = {Keywords: Narrowing, Multiset Narrowing, Unifiability, Reachability} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Carl Kwan and Warren A. Hunt Jr.. Formalizing the Cholesky Factorization Theorem. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kwan_et_al:LIPIcs.ITP.2024.25, author = {Kwan, Carl and Hunt Jr., Warren A.}, title = {{Formalizing the Cholesky Factorization Theorem}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {25:1--25:16}, 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.25}, URN = {urn:nbn:de:0030-drops-207532}, doi = {10.4230/LIPIcs.ITP.2024.25}, annote = {Keywords: Numerical linear algebra, Cholesky factorization theorem, Matrix decomposition, Automated reasoning, ACL2} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Patrick Massot. Teaching Mathematics Using Lean and Controlled Natural Language. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{massot:LIPIcs.ITP.2024.27, 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} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Karol Pąk and Cezary Kaliszyk. Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{pak_et_al:LIPIcs.ITP.2024.29, author = {P\k{a}k, Karol and Kaliszyk, Cezary}, title = {{Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {29:1--29: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.29}, URN = {urn:nbn:de:0030-drops-207573}, doi = {10.4230/LIPIcs.ITP.2024.29}, annote = {Keywords: Surreal numbers, Conway normal form, Mizar} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Sam Ezeh. Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 41:1-41:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ezeh:LIPIcs.ITP.2024.41, 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} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Teppei Saito and Nao Hirokawa. Simulating Dependency Pairs by Semantic Labeling. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{saito_et_al:LIPIcs.FSCD.2024.13, author = {Saito, Teppei and Hirokawa, Nao}, title = {{Simulating Dependency Pairs by Semantic Labeling}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {13:1--13:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.13}, URN = {urn:nbn:de:0030-drops-203423}, doi = {10.4230/LIPIcs.FSCD.2024.13}, annote = {Keywords: Term rewriting, Relative termination, Semantic labeling, Dependency pairs} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Franz Baader and Jürgen Giesl. On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{baader_et_al:LIPIcs.FSCD.2024.16, author = {Baader, Franz and Giesl, J\"{u}rgen}, title = {{On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {16:1--16:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.16}, URN = {urn:nbn:de:0030-drops-203454}, doi = {10.4230/LIPIcs.FSCD.2024.16}, annote = {Keywords: Rewriting, Termination, Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21, author = {Felicissimo, Thiago and Winterhalter, Th\'{e}o}, title = {{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {21:1--21:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21}, URN = {urn:nbn:de:0030-drops-203503}, doi = {10.4230/LIPIcs.FSCD.2024.21}, annote = {Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27, author = {Thiemann, Ren\'{e} and Yamada, Akihisa}, title = {{A Verified Algorithm for Deciding Pattern Completeness}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {27:1--27:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.27}, URN = {urn:nbn:de:0030-drops-203566}, doi = {10.4230/LIPIcs.FSCD.2024.27}, annote = {Keywords: Isabelle/HOL, pattern matching, term rewriting} }
Feedback for Dagstuhl Publishing