LIPIcs, Volume 309, ITP 2024

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