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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
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.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} }
Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{forster_et_al:LIPIcs.ITP.2022.12, author = {Forster, Yannick and Kunze, Fabian and Lauermann, Nils}, title = {{Synthetic Kolmogorov Complexity in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {12:1--12: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.12}, URN = {urn:nbn:de:0030-drops-167219}, doi = {10.4230/LIPIcs.ITP.2022.12}, annote = {Keywords: Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq} }
Asta Halkjær From and Frederik Krogsdal Jacobsen. Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{from_et_al:LIPIcs.ITP.2022.13, author = {From, Asta Halkj{\ae}r and Jacobsen, Frederik Krogsdal}, title = {{Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {13:1--13:22}, 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.13}, URN = {urn:nbn:de:0030-drops-167221}, doi = {10.4230/LIPIcs.ITP.2022.13}, annote = {Keywords: Isabelle/HOL, SeCaV, First-Order Logic, Prover, Soundness, Completeness} }
María Inés de Frutos-Fernández. Formalizing the Ring of Adèles of a Global Field. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{defrutosfernandez:LIPIcs.ITP.2022.14, author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s}, title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {14:1--14: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.14}, URN = {urn:nbn:de:0030-drops-167232}, doi = {10.4230/LIPIcs.ITP.2022.14}, annote = {Keywords: formal math, algebraic number theory, class field theory, Lean, mathlib} }
Arve Gengelbach and Johannes Åman Pohjola. A Verified Cyclicity Checker: For Theories with Overloaded Constants. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gengelbach_et_al:LIPIcs.ITP.2022.15, author = {Gengelbach, Arve and \r{A}man Pohjola, Johannes}, title = {{A Verified Cyclicity Checker: For Theories with Overloaded Constants}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {15:1--15: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.15}, URN = {urn:nbn:de:0030-drops-167240}, doi = {10.4230/LIPIcs.ITP.2022.15}, annote = {Keywords: cyclicity, non-termination, ad-hoc overloading, definitions, Isabelle/HOL} }
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{goertzel_et_al:LIPIcs.ITP.2022.16, author = {Goertzel, Zarathustra A. and Jakub\r{u}v, Jan and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Miroslav and Piepenbrock, Jelle and Urban, Josef}, title = {{The Isabelle ENIGMA}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {16:1--16: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.16}, URN = {urn:nbn:de:0030-drops-167253}, doi = {10.4230/LIPIcs.ITP.2022.16}, annote = {Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer} }
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala. Accelerating Verified-Compiler Development with a Verified Rewriting Engine. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gross_et_al:LIPIcs.ITP.2022.17, author = {Gross, Jason and Erbsen, Andres and Philipoom, Jade and Poddar-Agrawal, Miraya and Chlipala, Adam}, title = {{Accelerating Verified-Compiler Development with a Verified Rewriting Engine}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {17:1--17: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.17}, URN = {urn:nbn:de:0030-drops-167262}, doi = {10.4230/LIPIcs.ITP.2022.17}, annote = {Keywords: compiler verification, rewriting engines, cryptography} }
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala. Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gross_et_al:LIPIcs.ITP.2022.18, author = {Gross, Jason and Zimmermann, Th\'{e}o and Poddar-Agrawal, Miraya and Chlipala, Adam}, title = {{Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {18:1--18: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.18}, URN = {urn:nbn:de:0030-drops-167273}, doi = {10.4230/LIPIcs.ITP.2022.18}, annote = {Keywords: debugging, automatic test-case reduction, Coq, bug minimizer} }
Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of Dyadic First-Order Logic in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{hostert_et_al:LIPIcs.ITP.2022.19, author = {Hostert, Johannes and Dudenhefner, Andrej and Kirst, Dominik}, title = {{Undecidability of Dyadic First-Order Logic in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {19:1--19: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.19}, URN = {urn:nbn:de:0030-drops-167280}, doi = {10.4230/LIPIcs.ITP.2022.19}, annote = {Keywords: undecidability, synthetic computability, first-order logic, Coq} }
Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen. Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{kanabar_et_al:LIPIcs.ITP.2022.20, author = {Kanabar, Hrutvik and Fox, Anthony C. J. and Myreen, Magnus O.}, title = {{Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {20:1--20:22}, 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.20}, URN = {urn:nbn:de:0030-drops-167295}, doi = {10.4230/LIPIcs.ITP.2022.20}, annote = {Keywords: Compiler verification, ISA specification, HOL4, interactive theorem proving} }
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} }
Dominik Kirst. Computational Back-And-Forth Arguments in Constructive Type Theory. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 22:1-22:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{kirst:LIPIcs.ITP.2022.22, author = {Kirst, Dominik}, title = {{Computational Back-And-Forth Arguments in Constructive Type Theory}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {22:1--22:12}, 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.22}, URN = {urn:nbn:de:0030-drops-167311}, doi = {10.4230/LIPIcs.ITP.2022.22}, annote = {Keywords: back-and-forth method, computable isomorphisms, Coq} }
Yury Kudryashov. Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{kudryashov:LIPIcs.ITP.2022.23, author = {Kudryashov, Yury}, title = {{Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {23:1--23: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.23}, URN = {urn:nbn:de:0030-drops-167326}, doi = {10.4230/LIPIcs.ITP.2022.23}, annote = {Keywords: divergence theorem, Green’s theorem, Gauge integral, Cauchy integral formula, Cauchy-Goursat theorem, complex analysis} }
Peter Lammich. Refinement of Parallel Algorithms down to LLVM. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{lammich:LIPIcs.ITP.2022.24, author = {Lammich, Peter}, title = {{Refinement of Parallel Algorithms down to LLVM}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {24:1--24: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.24}, URN = {urn:nbn:de:0030-drops-167333}, doi = {10.4230/LIPIcs.ITP.2022.24}, annote = {Keywords: Isabelle, Concurrent Separation Logic, Parallel Sorting, LLVM} }
Nicolas Magaud. Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{magaud:LIPIcs.ITP.2022.25, author = {Magaud, Nicolas}, title = {{Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {25:1--25: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.25}, URN = {urn:nbn:de:0030-drops-167349}, doi = {10.4230/LIPIcs.ITP.2022.25}, annote = {Keywords: Coq, projective geometry, finite models, spreads, packings, PG(3, 2)} }
Karol Pąk and Cezary Kaliszyk. Formalizing a Diophantine Representation of the Set of Prime Numbers. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 26:1-26:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{pak_et_al:LIPIcs.ITP.2022.26, author = {P\k{a}k, Karol and Kaliszyk, Cezary}, title = {{Formalizing a Diophantine Representation of the Set of Prime Numbers}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {26:1--26:8}, 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.26}, URN = {urn:nbn:de:0030-drops-167350}, doi = {10.4230/LIPIcs.ITP.2022.26}, annote = {Keywords: DPRM theorem, Polynomial reduction, prime numbers} }
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A Verified, End-To-End Compiler for a Choreographic Language. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{pohjola_et_al:LIPIcs.ITP.2022.27, author = {Pohjola, Johannes \r{A}man and G\'{o}mez-Londo\~{n}o, Alejandro and Shaker, James and Norrish, Michael}, title = {{Kalas: A Verified, End-To-End Compiler for a Choreographic Language}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {27:1--27: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.27}, URN = {urn:nbn:de:0030-drops-167368}, doi = {10.4230/LIPIcs.ITP.2022.27}, annote = {Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification} }
Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos. Deeper Shallow Embeddings. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{prinz_et_al:LIPIcs.ITP.2022.28, author = {Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas}, title = {{Deeper Shallow Embeddings}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {28:1--28: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.28}, URN = {urn:nbn:de:0030-drops-167379}, doi = {10.4230/LIPIcs.ITP.2022.28}, annote = {Keywords: type theory, shallow embedding, deep embedding, Agda} }
Kazuhiko Sakaguchi. Reflexive Tactics for Algebra, Revisited. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{sakaguchi:LIPIcs.ITP.2022.29, author = {Sakaguchi, Kazuhiko}, title = {{Reflexive Tactics for Algebra, Revisited}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {29:1--29:22}, 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.29}, URN = {urn:nbn:de:0030-drops-167385}, doi = {10.4230/LIPIcs.ITP.2022.29}, annote = {Keywords: Coq, Elpi, \lambdaProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection} }
Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu. Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{stoughton_et_al:LIPIcs.ITP.2022.30, author = {Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao}, title = {{Formalizing Algorithmic Bounds in the Query Model in EasyCrypt}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {30:1--30: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.30}, URN = {urn:nbn:de:0030-drops-167399}, doi = {10.4230/LIPIcs.ITP.2022.30}, annote = {Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt} }
Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun. Formalization of a Stochastic Approximation Theorem. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{vajjha_et_al:LIPIcs.ITP.2022.31, author = {Vajjha, Koundinya and Trager, Barry and Shinnar, Avraham and Pestun, Vasily}, title = {{Formalization of a Stochastic Approximation Theorem}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {31:1--31: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.31}, URN = {urn:nbn:de:0030-drops-167402}, doi = {10.4230/LIPIcs.ITP.2022.31}, annote = {Keywords: Formal Verification, Stochastic Approximation, Stochastic Processes, Probability Theory, Optimization Algorithms} }
Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas. Mechanizing Soundness of Off-Policy Evaluation. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{yeager_et_al:LIPIcs.ITP.2022.32, author = {Yeager, Jared and Moss, J. Eliot B. and Norrish, Michael and Thomas, Philip S.}, title = {{Mechanizing Soundness of Off-Policy Evaluation}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {32:1--32: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.32}, URN = {urn:nbn:de:0030-drops-167413}, doi = {10.4230/LIPIcs.ITP.2022.32}, annote = {Keywords: Formal Methods, HOL4, Reinforcement Learning, Off-Policy Evaluation, Concentration Inequality, Hoeffding} }
Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia. Compositional Verification of Interacting Systems Using Event Monads. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{zhan_et_al:LIPIcs.ITP.2022.33, author = {Zhan, Bohua and Lv, Yi and Wang, Shuling and Zhao, Gehang and Hao, Jifeng and Ye, Hong and Xia, Bican}, title = {{Compositional Verification of Interacting Systems Using Event Monads}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {33:1--33: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.33}, URN = {urn:nbn:de:0030-drops-167420}, doi = {10.4230/LIPIcs.ITP.2022.33}, annote = {Keywords: Hoare Logic, Compositional Verification, Events} }