<h2>LIPIcs, Volume 193, ITP 2021</h2>
<ul>
<li>
<span class="authors">Liron Cohen and Cezary Kaliszyk</span>
<span class="title">LIPIcs, Volume 193, ITP 2021, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021">10.4230/LIPIcs.ITP.2021</a>
</li>
<li>
<span class="authors">Liron Cohen and Cezary Kaliszyk</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.0">10.4230/LIPIcs.ITP.2021.0</a>
</li>
<li>
<span class="authors">Magnus O. Myreen</span>
<span class="title">The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.1">10.4230/LIPIcs.ITP.2021.1</a>
</li>
<li>
<span class="authors">Nadia Polikarpova</span>
<span class="title">Synthesis of Safe Pointer-Manipulating Programs (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.2">10.4230/LIPIcs.ITP.2021.2</a>
</li>
<li>
<span class="authors">Andrei Popescu, Thomas Bauereiss, and Peter Lammich</span>
<span class="title">Bounded-Deducibility Security (Invited Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.3">10.4230/LIPIcs.ITP.2021.3</a>
</li>
<li>
<span class="authors">Edward W. Ayers, Mateja Jamnik, and W. T. Gowers</span>
<span class="title">A Graphical User Interface Framework for Formal Verification</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.4">10.4230/LIPIcs.ITP.2021.4</a>
</li>
<li>
<span class="authors">Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio</span>
<span class="title">A Formalization of Dedekind Domains and Class Groups of Global Fields</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.5">10.4230/LIPIcs.ITP.2021.5</a>
</li>
<li>
<span class="authors">Seulkee Baek</span>
<span class="title">A Formally Verified Checker for First-Order Proofs</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.6">10.4230/LIPIcs.ITP.2021.6</a>
</li>
<li>
<span class="authors">Christoph Benzmüller and David Fuenmayor</span>
<span class="title">Value-Oriented Legal Argumentation in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.7">10.4230/LIPIcs.ITP.2021.7</a>
</li>
<li>
<span class="authors">Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub</span>
<span class="title">Unsolvability of the Quintic Formalized in Dependent Type Theory</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.8">10.4230/LIPIcs.ITP.2021.8</a>
</li>
<li>
<span class="authors">Frédéric Besson</span>
<span class="title">Itauto: An Extensible Intuitionistic SAT Solver</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.9">10.4230/LIPIcs.ITP.2021.9</a>
</li>
<li>
<span class="authors">Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel</span>
<span class="title">Verified Progress Tracking for Timely Dataflow</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.10">10.4230/LIPIcs.ITP.2021.10</a>
</li>
<li>
<span class="authors">Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz</span>
<span class="title">Syntactic-Semantic Form of Mizar Articles</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.11">10.4230/LIPIcs.ITP.2021.11</a>
</li>
<li>
<span class="authors">Joshua Chen</span>
<span class="title">Homotopy Type Theory in Isabelle</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.12">10.4230/LIPIcs.ITP.2021.12</a>
</li>
<li>
<span class="authors">Luca Ciccone, Francesco Dagnino, and Elena Zucca</span>
<span class="title">Flexible Coinduction in Agda</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.13">10.4230/LIPIcs.ITP.2021.13</a>
</li>
<li>
<span class="authors">Katherine Cordwell, Yong Kiam Tan, and André Platzer</span>
<span class="title">A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.14">10.4230/LIPIcs.ITP.2021.14</a>
</li>
<li>
<span class="authors">Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti</span>
<span class="title">Formalising a Turing-Complete Choreographic Language in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.15">10.4230/LIPIcs.ITP.2021.15</a>
</li>
<li>
<span class="authors">Adrian De Lon, Peter Koepke, and Anton Lorenzen</span>
<span class="title">A Natural Formalization of the Mutilated Checkerboard Problem in Naproche</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.16">10.4230/LIPIcs.ITP.2021.16</a>
</li>
<li>
<span class="authors">Christian Doczkal</span>
<span class="title">A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.17">10.4230/LIPIcs.ITP.2021.17</a>
</li>
<li>
<span class="authors">Floris van Doorn</span>
<span class="title">Formalized Haar Measure</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.18">10.4230/LIPIcs.ITP.2021.18</a>
</li>
<li>
<span class="authors">Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke</span>
<span class="title">A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.19">10.4230/LIPIcs.ITP.2021.19</a>
</li>
<li>
<span class="authors">Lennard Gäher and Fabian Kunze</span>
<span class="title">Mechanising Complexity Theory: The Cook-Levin Theorem in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.20">10.4230/LIPIcs.ITP.2021.20</a>
</li>
<li>
<span class="authors">Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks</span>
<span class="title">Proving Quantum Programs Correct</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.21">10.4230/LIPIcs.ITP.2021.21</a>
</li>
<li>
<span class="authors">Štěpán Holub and Štěpán Starosta</span>
<span class="title">Formalization of Basic Combinatorics on Words</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.22">10.4230/LIPIcs.ITP.2021.22</a>
</li>
<li>
<span class="authors">Dominik Kirst and Marc Hermes</span>
<span class="title">Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.23">10.4230/LIPIcs.ITP.2021.23</a>
</li>
<li>
<span class="authors">Meven Lennon-Bertrand</span>
<span class="title">Complete Bidirectional Typing for the Calculus of Inductive Constructions</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.24">10.4230/LIPIcs.ITP.2021.24</a>
</li>
<li>
<span class="authors">Andreas Lochbihler</span>
<span class="title">A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.25">10.4230/LIPIcs.ITP.2021.25</a>
</li>
<li>
<span class="authors">Marco Maggesi and Cosimo Perini Brogi</span>
<span class="title">A Formal Proof of Modal Completeness for Provability Logic</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.26">10.4230/LIPIcs.ITP.2021.26</a>
</li>
<li>
<span class="authors">Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane A. Almeida, Andréia B. Avelar, and Thiago M. Ferreira Ramos</span>
<span class="title">Formal Verification of Termination Criteria for First-Order Recursive Functions</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.27">10.4230/LIPIcs.ITP.2021.27</a>
</li>
<li>
<span class="authors">Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh</span>
<span class="title">Verified Double Sided Auctions for Financial Markets</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.28">10.4230/LIPIcs.ITP.2021.28</a>
</li>
<li>
<span class="authors">Pierre Nigron and Pierre-Évariste Dagand</span>
<span class="title">Reaching for the Star: Tale of a Monad in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.29">10.4230/LIPIcs.ITP.2021.29</a>
</li>
<li>
<span class="authors">Konrad Slind</span>
<span class="title">Specifying Message Formats with Contiguity Types</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.30">10.4230/LIPIcs.ITP.2021.30</a>
</li>
<li>
<span class="authors">Laurent Théry</span>
<span class="title">Proof Pearl : Playing with the Tower of Hanoi Formally</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.31">10.4230/LIPIcs.ITP.2021.31</a>
</li>
<li>
<span class="authors">Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic</span>
<span class="title">Verifying an HTTP Key-Value Server with Interaction Trees and VST</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2021.32">10.4230/LIPIcs.ITP.2021.32</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