<h2>LIPIcs, Volume 237, ITP 2022</h2>
<ul>
<li>
<span class="authors">June Andronick and Leonardo de Moura</span>
<span class="title">LIPIcs, Volume 237, ITP 2022, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022">10.4230/LIPIcs.ITP.2022</a>
</li>
<li>
<span class="authors">June Andronick and Leonardo de Moura</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.0">10.4230/LIPIcs.ITP.2022.0</a>
</li>
<li>
<span class="authors">Amy Felty</span>
<span class="title">Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.1">10.4230/LIPIcs.ITP.2022.1</a>
</li>
<li>
<span class="authors">Bohua Zhan</span>
<span class="title">User Interface Design in the HolPy Theorem Prover (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.2">10.4230/LIPIcs.ITP.2022.2</a>
</li>
<li>
<span class="authors">Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell</span>
<span class="title">Candle: A Verified Implementation of HOL Light</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.3">10.4230/LIPIcs.ITP.2022.3</a>
</li>
<li>
<span class="authors">Anne Baanen</span>
<span class="title">Use and Abuse of Instance Parameters in the Lean Mathematical Library</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.4">10.4230/LIPIcs.ITP.2022.4</a>
</li>
<li>
<span class="authors">Jagadish Bapanapally and Ruben Gamboa</span>
<span class="title">A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.5">10.4230/LIPIcs.ITP.2022.5</a>
</li>
<li>
<span class="authors">Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin</span>
<span class="title">Dandelion: Certified Approximations of Elementary Functions</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.6">10.4230/LIPIcs.ITP.2022.6</a>
</li>
<li>
<span class="authors">Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab</span>
<span class="title">The Zoo of Lambda-Calculus Reduction Strategies, And Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.7">10.4230/LIPIcs.ITP.2022.7</a>
</li>
<li>
<span class="authors">Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel</span>
<span class="title">Seventeen Provers Under the Hammer</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.8">10.4230/LIPIcs.ITP.2022.8</a>
</li>
<li>
<span class="authors">Yaël Dillies and Bhavik Mehta</span>
<span class="title">Formalising Szemerédi’s Regularity Lemma in Lean</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.9">10.4230/LIPIcs.ITP.2022.9</a>
</li>
<li>
<span class="authors">Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth</span>
<span class="title">Formalized functional analysis with semilinear maps</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.10">10.4230/LIPIcs.ITP.2022.10</a>
</li>
<li>
<span class="authors">Chelsea Edmonds and Lawrence C. Paulson</span>
<span class="title">Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.11">10.4230/LIPIcs.ITP.2022.11</a>
</li>
<li>
<span class="authors">Yannick Forster, Fabian Kunze, and Nils Lauermann</span>
<span class="title">Synthetic Kolmogorov Complexity in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.12">10.4230/LIPIcs.ITP.2022.12</a>
</li>
<li>
<span class="authors">Asta Halkjær From and Frederik Krogsdal Jacobsen</span>
<span class="title">Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.13">10.4230/LIPIcs.ITP.2022.13</a>
</li>
<li>
<span class="authors">María Inés de Frutos-Fernández</span>
<span class="title">Formalizing the Ring of Adèles of a Global Field</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.14">10.4230/LIPIcs.ITP.2022.14</a>
</li>
<li>
<span class="authors">Arve Gengelbach and Johannes Åman Pohjola</span>
<span class="title">A Verified Cyclicity Checker: For Theories with Overloaded Constants</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.15">10.4230/LIPIcs.ITP.2022.15</a>
</li>
<li>
<span class="authors">Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban</span>
<span class="title">The Isabelle ENIGMA</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.16">10.4230/LIPIcs.ITP.2022.16</a>
</li>
<li>
<span class="authors">Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala</span>
<span class="title">Accelerating Verified-Compiler Development with a Verified Rewriting Engine</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.17">10.4230/LIPIcs.ITP.2022.17</a>
</li>
<li>
<span class="authors">Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala</span>
<span class="title">Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.18">10.4230/LIPIcs.ITP.2022.18</a>
</li>
<li>
<span class="authors">Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst</span>
<span class="title">Undecidability of Dyadic First-Order Logic in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.19">10.4230/LIPIcs.ITP.2022.19</a>
</li>
<li>
<span class="authors">Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen</span>
<span class="title">Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.20">10.4230/LIPIcs.ITP.2022.20</a>
</li>
<li>
<span class="authors">Emin Karayel</span>
<span class="title">Formalization of Randomized Approximation Algorithms for Frequency Moments</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.21">10.4230/LIPIcs.ITP.2022.21</a>
</li>
<li>
<span class="authors">Dominik Kirst</span>
<span class="title">Computational Back-And-Forth Arguments in Constructive Type Theory</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.22">10.4230/LIPIcs.ITP.2022.22</a>
</li>
<li>
<span class="authors">Yury Kudryashov</span>
<span class="title">Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.23">10.4230/LIPIcs.ITP.2022.23</a>
</li>
<li>
<span class="authors">Peter Lammich</span>
<span class="title">Refinement of Parallel Algorithms down to LLVM</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.24">10.4230/LIPIcs.ITP.2022.24</a>
</li>
<li>
<span class="authors">Nicolas Magaud</span>
<span class="title">Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.25">10.4230/LIPIcs.ITP.2022.25</a>
</li>
<li>
<span class="authors">Karol Pąk and Cezary Kaliszyk</span>
<span class="title">Formalizing a Diophantine Representation of the Set of Prime Numbers</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.26">10.4230/LIPIcs.ITP.2022.26</a>
</li>
<li>
<span class="authors">Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish</span>
<span class="title">Kalas: A Verified, End-To-End Compiler for a Choreographic Language</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.27">10.4230/LIPIcs.ITP.2022.27</a>
</li>
<li>
<span class="authors">Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos</span>
<span class="title">Deeper Shallow Embeddings</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.28">10.4230/LIPIcs.ITP.2022.28</a>
</li>
<li>
<span class="authors">Kazuhiko Sakaguchi</span>
<span class="title">Reflexive Tactics for Algebra, Revisited</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.29">10.4230/LIPIcs.ITP.2022.29</a>
</li>
<li>
<span class="authors">Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu</span>
<span class="title">Formalizing Algorithmic Bounds in the Query Model in EasyCrypt</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.30">10.4230/LIPIcs.ITP.2022.30</a>
</li>
<li>
<span class="authors">Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun</span>
<span class="title">Formalization of a Stochastic Approximation Theorem</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.31">10.4230/LIPIcs.ITP.2022.31</a>
</li>
<li>
<span class="authors">Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas</span>
<span class="title">Mechanizing Soundness of Off-Policy Evaluation</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.32">10.4230/LIPIcs.ITP.2022.32</a>
</li>
<li>
<span class="authors">Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia</span>
<span class="title">Compositional Verification of Interacting Systems Using Event Monads</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2022.33">10.4230/LIPIcs.ITP.2022.33</a>
</li>
</ul>
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing