<h2>LIPIcs, Volume 309, ITP 2024</h2>
<ul>
<li>
<span class="authors">Yves Bertot, Temur Kutsia, and Michael Norrish</span>
<span class="title">LIPIcs, Volume 309, ITP 2024, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024">10.4230/LIPIcs.ITP.2024</a>
</li>
<li>
<span class="authors">Yves Bertot, Temur Kutsia, and Michael Norrish</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.0">10.4230/LIPIcs.ITP.2024.0</a>
</li>
<li>
<span class="authors">Tobias Nipkow</span>
<span class="title">Alpha-Beta Pruning Verified (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.1">10.4230/LIPIcs.ITP.2024.1</a>
</li>
<li>
<span class="authors">Frédéric Blanqui</span>
<span class="title">Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.2">10.4230/LIPIcs.ITP.2024.2</a>
</li>
<li>
<span class="authors">Mohammad Abdulaziz and Thomas Ammer</span>
<span class="title">A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.3">10.4230/LIPIcs.ITP.2024.3</a>
</li>
<li>
<span class="authors">Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, and Kathrin Stark</span>
<span class="title">Taming Differentiable Logics with Coq Formalisation</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.4">10.4230/LIPIcs.ITP.2024.4</a>
</li>
<li>
<span class="authors">Reynald Affeldt and Zachary Stone</span>
<span class="title">A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.5">10.4230/LIPIcs.ITP.2024.5</a>
</li>
<li>
<span class="authors">Dagur Asgeirsson</span>
<span class="title">Towards Solid Abelian Groups: A Formal Proof of Nöbeling’s Theorem</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.6">10.4230/LIPIcs.ITP.2024.6</a>
</li>
<li>
<span class="authors">Benoît Ballenghien and Burkhart Wolff</span>
<span class="title">An Operational Semantics in Isabelle/HOL-CSP</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.7">10.4230/LIPIcs.ITP.2024.7</a>
</li>
<li>
<span class="authors">Henning Basold, Peter Bruin, and Dominique Lawson</span>
<span class="title">The Directed Van Kampen Theorem in Lean</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.8">10.4230/LIPIcs.ITP.2024.8</a>
</li>
<li>
<span class="authors">Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser</span>
<span class="title">Verifying Peephole Rewriting in SSA Compiler IRs</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.9">10.4230/LIPIcs.ITP.2024.9</a>
</li>
<li>
<span class="authors">Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad</span>
<span class="title">Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.10">10.4230/LIPIcs.ITP.2024.10</a>
</li>
<li>
<span class="authors">Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón</span>
<span class="title">A Formalization of the General Theory of Quaternions</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.11">10.4230/LIPIcs.ITP.2024.11</a>
</li>
<li>
<span class="authors">Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret</span>
<span class="title">A Modular Formalization of Superposition in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.12">10.4230/LIPIcs.ITP.2024.12</a>
</li>
<li>
<span class="authors">Burak Ekici and Nobuko Yoshida</span>
<span class="title">Completeness of Asynchronous Session Tree Subtyping in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.13">10.4230/LIPIcs.ITP.2024.13</a>
</li>
<li>
<span class="authors">Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond</span>
<span class="title">End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.14">10.4230/LIPIcs.ITP.2024.14</a>
</li>
<li>
<span class="authors">Jacques Garrigue and Takafumi Saikawa</span>
<span class="title">Typed Compositional Quantum Computation with Lenses</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.15">10.4230/LIPIcs.ITP.2024.15</a>
</li>
<li>
<span class="authors">Thibault Gauthier and Chad E. Brown</span>
<span class="title">A Formal Proof of R(4,5)=25</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.16">10.4230/LIPIcs.ITP.2024.16</a>
</li>
<li>
<span class="authors">Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala</span>
<span class="title">Verifying Software Emulation of an Unsupported Hardware Instruction</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.17">10.4230/LIPIcs.ITP.2024.17</a>
</li>
<li>
<span class="authors">Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak</span>
<span class="title">Mechanized HOL Reasoning in Set Theory</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.18">10.4230/LIPIcs.ITP.2024.18</a>
</li>
<li>
<span class="authors">Marc Hermes and Robbert Krebbers</span>
<span class="title">Modular Verification of Intrusive List and Tree Data Structures in Separation Logic</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.19">10.4230/LIPIcs.ITP.2024.19</a>
</li>
<li>
<span class="authors">Dennis Hilhorst and Paige Randall North</span>
<span class="title">Formalizing the Algebraic Small Object Argument in UniMath</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.20">10.4230/LIPIcs.ITP.2024.20</a>
</li>
<li>
<span class="authors">Michikazu Hirata</span>
<span class="title">A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.21">10.4230/LIPIcs.ITP.2024.21</a>
</li>
<li>
<span class="authors">Fabian Huch and Makarius Wenzel</span>
<span class="title">Distributed Parallel Build for the Isabelle Archive of Formal Proofs</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.22">10.4230/LIPIcs.ITP.2024.22</a>
</li>
<li>
<span class="authors">Vincent Jackson, Toby Murray, and Christine Rizkallah</span>
<span class="title">A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.23">10.4230/LIPIcs.ITP.2024.23</a>
</li>
<li>
<span class="authors">Dohan Kim</span>
<span class="title">An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.24">10.4230/LIPIcs.ITP.2024.24</a>
</li>
<li>
<span class="authors">Carl Kwan and Warren A. Hunt Jr.</span>
<span class="title">Formalizing the Cholesky Factorization Theorem</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.25">10.4230/LIPIcs.ITP.2024.25</a>
</li>
<li>
<span class="authors">Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter</span>
<span class="title">The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.26">10.4230/LIPIcs.ITP.2024.26</a>
</li>
<li>
<span class="authors">Patrick Massot</span>
<span class="title">Teaching Mathematics Using Lean and Controlled Natural Language</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.27">10.4230/LIPIcs.ITP.2024.27</a>
</li>
<li>
<span class="authors">Kai Obendrauf, Anne Baanen, Patrick Koopmann, and Vera Stebletsova</span>
<span class="title">Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.28">10.4230/LIPIcs.ITP.2024.28</a>
</li>
<li>
<span class="authors">Karol Pąk and Cezary Kaliszyk</span>
<span class="title">Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.29">10.4230/LIPIcs.ITP.2024.29</a>
</li>
<li>
<span class="authors">Sewon Park and Holger Thies</span>
<span class="title">A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.30">10.4230/LIPIcs.ITP.2024.30</a>
</li>
<li>
<span class="authors">Martin Rau and Tobias Nipkow</span>
<span class="title">A Verified Earley Parser</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.31">10.4230/LIPIcs.ITP.2024.31</a>
</li>
<li>
<span class="authors">Hannes Saffrich</span>
<span class="title">Abstractions for Multi-Sorted Substitutions</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.32">10.4230/LIPIcs.ITP.2024.32</a>
</li>
<li>
<span class="authors">Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer</span>
<span class="title">Correctly Compiling Proofs About Programs Without Proving Compilers Correct</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.33">10.4230/LIPIcs.ITP.2024.33</a>
</li>
<li>
<span class="authors">Mallku Soldevila, Rodrigo Ribeiro, and Beta Ziliani</span>
<span class="title">Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.34">10.4230/LIPIcs.ITP.2024.34</a>
</li>
<li>
<span class="authors">Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule</span>
<span class="title">Formal Verification of the Empty Hexagon Number</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.35">10.4230/LIPIcs.ITP.2024.35</a>
</li>
<li>
<span class="authors">Andrew Tolmach, Chris Chhak, and Sean Anderson</span>
<span class="title">Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.36">10.4230/LIPIcs.ITP.2024.36</a>
</li>
<li>
<span class="authors">Floris van Doorn and Heather Macbeth</span>
<span class="title">Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.37">10.4230/LIPIcs.ITP.2024.37</a>
</li>
<li>
<span class="authors">Max Zeuner and Matthias Hutzler</span>
<span class="title">The Functor of Points Approach to Schemes in Cubical Agda</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.38">10.4230/LIPIcs.ITP.2024.38</a>
</li>
<li>
<span class="authors">Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann</span>
<span class="title">Robust Mean Estimation by All Means (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.39">10.4230/LIPIcs.ITP.2024.39</a>
</li>
<li>
<span class="authors">Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li</span>
<span class="title">Formalising Half of a Graduate Textbook on Number Theory (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.40">10.4230/LIPIcs.ITP.2024.40</a>
</li>
<li>
<span class="authors">Sam Ezeh</span>
<span class="title">Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2024.41">10.4230/LIPIcs.ITP.2024.41</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