<h2>LIPIcs, Volume 268, ITP 2023</h2>
<ul>
<li>
<span class="authors">Adam Naumowicz and René Thiemann</span>
<span class="title">LIPIcs, Volume 268, ITP 2023, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023">10.4230/LIPIcs.ITP.2023</a>
</li>
<li>
<span class="authors">Adam Naumowicz and René Thiemann</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.0">10.4230/LIPIcs.ITP.2023.0</a>
</li>
<li>
<span class="authors">Angeliki Koutsoukou-Argyraki</span>
<span class="title">Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.1">10.4230/LIPIcs.ITP.2023.1</a>
</li>
<li>
<span class="authors">Robbert Krebbers</span>
<span class="title">Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.2">10.4230/LIPIcs.ITP.2023.2</a>
</li>
<li>
<span class="authors">Mohammad Abdulaziz and Christoph Madlener</span>
<span class="title">A Formal Analysis of RANKING</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.3">10.4230/LIPIcs.ITP.2023.3</a>
</li>
<li>
<span class="authors">Oskar Abrahamsson and Magnus O. Myreen</span>
<span class="title">Fast, Verified Computation for Candle</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.4">10.4230/LIPIcs.ITP.2023.4</a>
</li>
<li>
<span class="authors">Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen</span>
<span class="title">Formalizing Functions as Processes</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.5">10.4230/LIPIcs.ITP.2023.5</a>
</li>
<li>
<span class="authors">David Kurniadi Angdinata and Junyan Xu</span>
<span class="title">An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.6">10.4230/LIPIcs.ITP.2023.6</a>
</li>
<li>
<span class="authors">Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman</span>
<span class="title">A Proof-Producing Compiler for Blockchain Applications</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.7">10.4230/LIPIcs.ITP.2023.7</a>
</li>
<li>
<span class="authors">Roger Bosman, Georgios Karachalias, and Tom Schrijvers</span>
<span class="title">No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.8">10.4230/LIPIcs.ITP.2023.8</a>
</li>
<li>
<span class="authors">Mario Carneiro, Chad E. Brown, and Josef Urban</span>
<span class="title">Automated Theorem Proving for Metamath</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.9">10.4230/LIPIcs.ITP.2023.9</a>
</li>
<li>
<span class="authors">Mario Carneiro</span>
<span class="title">Reimplementing Mizar in Rust</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.10">10.4230/LIPIcs.ITP.2023.10</a>
</li>
<li>
<span class="authors">Luís Cruz-Filipe and Fabrizio Montesi</span>
<span class="title">Now It Compiles! Certified Automatic Repair of Uncompilable Protocols</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.11">10.4230/LIPIcs.ITP.2023.11</a>
</li>
<li>
<span class="authors">Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann</span>
<span class="title">Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.12">10.4230/LIPIcs.ITP.2023.12</a>
</li>
<li>
<span class="authors">María Inés de Frutos-Fernández</span>
<span class="title">Formalizing Norm Extensions and Applications to Number Theory</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.13">10.4230/LIPIcs.ITP.2023.13</a>
</li>
<li>
<span class="authors">Lawrence Dunn, Val Tannen, and Steve Zdancewic</span>
<span class="title">Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.14">10.4230/LIPIcs.ITP.2023.14</a>
</li>
<li>
<span class="authors">Martin Dvorak and Jasmin Blanchette</span>
<span class="title">Closure Properties of General Grammars – Formally Verified</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.15">10.4230/LIPIcs.ITP.2023.15</a>
</li>
<li>
<span class="authors">Jarl G. Taxerås Flaten</span>
<span class="title">Formalising Yoneda Ext in Univalent Foundations</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.16">10.4230/LIPIcs.ITP.2023.16</a>
</li>
<li>
<span class="authors">Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak</span>
<span class="title">LISA - A Modern Proof System</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.17">10.4230/LIPIcs.ITP.2023.17</a>
</li>
<li>
<span class="authors">Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato</span>
<span class="title">Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.18">10.4230/LIPIcs.ITP.2023.18</a>
</li>
<li>
<span class="authors">Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban</span>
<span class="title">MizAR 60 for Mizar 50</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.19">10.4230/LIPIcs.ITP.2023.19</a>
</li>
<li>
<span class="authors">Philipp Joram and Niccolò Veltri</span>
<span class="title">Constructive Final Semantics of Finite Bags</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.20">10.4230/LIPIcs.ITP.2023.20</a>
</li>
<li>
<span class="authors">Dominique Larchey-Wendling and Jean-François Monin</span>
<span class="title">Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.21">10.4230/LIPIcs.ITP.2023.21</a>
</li>
<li>
<span class="authors">Amelia Livingston</span>
<span class="title">Group Cohomology in the Lean Community Library</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.22">10.4230/LIPIcs.ITP.2023.22</a>
</li>
<li>
<span class="authors">Oliver Nash</span>
<span class="title">A Formalisation of Gallagher’s Ergodic Theorem</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.23">10.4230/LIPIcs.ITP.2023.23</a>
</li>
<li>
<span class="authors">Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner</span>
<span class="title">An Extensible User Interface for Lean 4</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.24">10.4230/LIPIcs.ITP.2023.24</a>
</li>
<li>
<span class="authors">Pierre Pomeret-Coquot, Hélène Fargier, and Érik Martin-Dorel</span>
<span class="title">Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.25">10.4230/LIPIcs.ITP.2023.25</a>
</li>
<li>
<span class="authors">Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer</span>
<span class="title">Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.26">10.4230/LIPIcs.ITP.2023.26</a>
</li>
<li>
<span class="authors">Chengsong Tan and Christian Urban</span>
<span class="title">POSIX Lexing with Bitcoded Derivatives</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.27">10.4230/LIPIcs.ITP.2023.27</a>
</li>
<li>
<span class="authors">Dawit Tirore, Jesper Bengtson, and Marco Carbone</span>
<span class="title">A Sound and Complete Projection for Global Types</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.28">10.4230/LIPIcs.ITP.2023.28</a>
</li>
<li>
<span class="authors">Balazs Toth and Tobias Nipkow</span>
<span class="title">Real-Time Double-Ended Queue Verified (Proof Pearl)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.29">10.4230/LIPIcs.ITP.2023.29</a>
</li>
<li>
<span class="authors">Niels van der Weide, Deivid Vale, and Cynthia Kop</span>
<span class="title">Certifying Higher-Order Polynomial Interpretations</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.30">10.4230/LIPIcs.ITP.2023.30</a>
</li>
<li>
<span class="authors">Niels F. W. Voorneveld</span>
<span class="title">Slice Nondeterminism</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.31">10.4230/LIPIcs.ITP.2023.31</a>
</li>
<li>
<span class="authors">Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel</span>
<span class="title">Foundational Verification of Stateful P4 Packet Processing</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.32">10.4230/LIPIcs.ITP.2023.32</a>
</li>
<li>
<span class="authors">Yiming Xu and Michael Norrish</span>
<span class="title">Dependently Sorted Theorem Proving for Mathematical Foundations</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.33">10.4230/LIPIcs.ITP.2023.33</a>
</li>
<li>
<span class="authors">Akihisa Yamada and Jérémy Dubut</span>
<span class="title">Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.34">10.4230/LIPIcs.ITP.2023.34</a>
</li>
<li>
<span class="authors">Jujian Zhang</span>
<span class="title">Formalising the Proj Construction in Lean</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.35">10.4230/LIPIcs.ITP.2023.35</a>
</li>
<li>
<span class="authors">Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi</span>
<span class="title">Fermat’s Last Theorem for Regular Primes (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.36">10.4230/LIPIcs.ITP.2023.36</a>
</li>
<li>
<span class="authors">Adam Grabowski and Artur Korniłowicz</span>
<span class="title">Implementing More Explicit Definitional Expansions in Mizar (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.37">10.4230/LIPIcs.ITP.2023.37</a>
</li>
<li>
<span class="authors">Christina Kohl and Aart Middeldorp</span>
<span class="title">Formalizing Almost Development Closed Critical Pairs (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2023.38">10.4230/LIPIcs.ITP.2023.38</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