LIPIcs, Volume 237
ITP 2022, August 7-10, 2022, Haifa, Israel
Editors: June Andronick and Leonardo de Moura
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24, author = {Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel}, title = {{An Extensible User Interface for Lean 4}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {24:1--24:20}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24}, URN = {urn:nbn:de:0030-drops-183991}, doi = {10.4230/LIPIcs.ITP.2023.24}, annote = {Keywords: user interfaces, human-computer interaction, Lean} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1-602, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@Proceedings{andronick_et_al:LIPIcs.ITP.2022, title = {{LIPIcs, Volume 237, ITP 2022, Complete Volume}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {1--602}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022}, URN = {urn:nbn:de:0030-drops-167080}, doi = {10.4230/LIPIcs.ITP.2022}, annote = {Keywords: LIPIcs, Volume 237, ITP 2022, Complete Volume} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{andronick_et_al:LIPIcs.ITP.2022.0, author = {Andronick, June and de Moura, Leonardo}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {0:i--0:x}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.0}, URN = {urn:nbn:de:0030-drops-167097}, doi = {10.4230/LIPIcs.ITP.2022.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Amy Felty. Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{felty:LIPIcs.ITP.2022.1, author = {Felty, Amy}, title = {{Modelling and Verifying Properties of Biological Neural Networks}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {1:1--1:2}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.1}, URN = {urn:nbn:de:0030-drops-167100}, doi = {10.4230/LIPIcs.ITP.2022.1}, annote = {Keywords: Neuronal networks, Model checking, Theorem proving, Coq} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Bohua Zhan. User Interface Design in the HolPy Theorem Prover (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{zhan:LIPIcs.ITP.2022.2, author = {Zhan, Bohua}, title = {{User Interface Design in the HolPy Theorem Prover}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {2:1--2:1}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.2}, URN = {urn:nbn:de:0030-drops-167117}, doi = {10.4230/LIPIcs.ITP.2022.2}, annote = {Keywords: Proof assistants, User interface, Proof automation} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2022.3, author = {Abrahamsson, Oskar and Myreen, Magnus O. and Kumar, Ramana and Sewell, Thomas}, title = {{Candle: A Verified Implementation of HOL Light}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {3:1--3:17}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.3}, URN = {urn:nbn:de:0030-drops-167126}, doi = {10.4230/LIPIcs.ITP.2022.3}, annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving} }
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-dev.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)
Jagadish Bapanapally and Ruben Gamboa. A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{bapanapally_et_al:LIPIcs.ITP.2022.5, author = {Bapanapally, Jagadish and Gamboa, Ruben}, title = {{A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {5:1--5:15}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.5}, URN = {urn:nbn:de:0030-drops-167142}, doi = {10.4230/LIPIcs.ITP.2022.5}, annote = {Keywords: ACL2(r), Banach-Tarski, Rotations} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{becker_et_al:LIPIcs.ITP.2022.6, author = {Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste}, title = {{Dandelion: Certified Approximations of Elementary Functions}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {6:1--6:19}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6}, URN = {urn:nbn:de:0030-drops-167155}, doi = {10.4230/LIPIcs.ITP.2022.6}, annote = {Keywords: elementary functions, approximation, certificate checking} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The Zoo of Lambda-Calculus Reduction Strategies, And Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7, author = {Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz}, title = {{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {7:1--7:19}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7}, URN = {urn:nbn:de:0030-drops-167165}, doi = {10.4230/LIPIcs.ITP.2022.7}, annote = {Keywords: Lambda calculus, Reduction strategies, Coq} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8, author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius}, title = {{Seventeen Provers Under the Hammer}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {8:1--8:18}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8}, URN = {urn:nbn:de:0030-drops-167178}, doi = {10.4230/LIPIcs.ITP.2022.8}, annote = {Keywords: Automatic theorem proving, interactive theorem proving, proof assistants} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Yaël Dillies and Bhavik Mehta. Formalising Szemerédi’s Regularity Lemma in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dillies_et_al:LIPIcs.ITP.2022.9, author = {Dillies, Ya\"{e}l and Mehta, Bhavik}, title = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {9:1--9:19}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.9}, URN = {urn:nbn:de:0030-drops-167185}, doi = {10.4230/LIPIcs.ITP.2022.9}, annote = {Keywords: Lean, formalisation, formal proof, graph theory, combinatorics, additive combinatorics, Szemer\'{e}di’s Regularity Lemma, Roth’s Theorem} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dupuis_et_al:LIPIcs.ITP.2022.10, author = {Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth, Heather}, title = {{Formalized functional analysis with semilinear maps}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {10:1--10:19}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.10}, URN = {urn:nbn:de:0030-drops-167191}, doi = {10.4230/LIPIcs.ITP.2022.10}, annote = {Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Chelsea Edmonds and Lawrence C. Paulson. Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{edmonds_et_al:LIPIcs.ITP.2022.11, author = {Edmonds, Chelsea and Paulson, Lawrence C.}, title = {{Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {11:1--11:19}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.11}, URN = {urn:nbn:de:0030-drops-167204}, doi = {10.4230/LIPIcs.ITP.2022.11}, annote = {Keywords: Isabelle/HOL, Mathematical Formalisation, Fisher’s Inequality, Linear Algebra, Formal Proof Techniques, Combinatorics} }
Feedback for Dagstuhl Publishing