<h2>LIPIcs, Volume 141, ITP 2019</h2>
<ul>
<li>
<span class="authors">John Harrison, John O'Leary, and Andrew Tolmach</span>
<span class="title">LIPIcs, Volume 141, ITP'19, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019">10.4230/LIPIcs.ITP.2019</a>
</li>
<li>
<span class="authors">John Harrison, John O'Leary, and Andrew Tolmach</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.0">10.4230/LIPIcs.ITP.2019.0</a>
</li>
<li>
<span class="authors">June Andronick</span>
<span class="title">A Million Lines of Proof About a Moving Target (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.1">10.4230/LIPIcs.ITP.2019.1</a>
</li>
<li>
<span class="authors">Kevin Buzzard</span>
<span class="title">What Makes a Mathematician Tick? (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.2">10.4230/LIPIcs.ITP.2019.2</a>
</li>
<li>
<span class="authors">Martin Dixon</span>
<span class="title">An Increasing Need for Formality (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.3">10.4230/LIPIcs.ITP.2019.3</a>
</li>
<li>
<span class="authors">Mohammad Abdulaziz, Charles Gretton, and Michael Norrish</span>
<span class="title">A Verified Compositional Algorithm for AI Planning</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.4">10.4230/LIPIcs.ITP.2019.4</a>
</li>
<li>
<span class="authors">Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka</span>
<span class="title">Proving Tree Algorithms for Succinct Data Structures</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.5">10.4230/LIPIcs.ITP.2019.5</a>
</li>
<li>
<span class="authors">Jeremy Avigad, Mario Carneiro, and Simon Hudon</span>
<span class="title">Data Types as Quotients of Polynomial Functors</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.6">10.4230/LIPIcs.ITP.2019.6</a>
</li>
<li>
<span class="authors">Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux</span>
<span class="title">Primitive Floats in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.7">10.4230/LIPIcs.ITP.2019.7</a>
</li>
<li>
<span class="authors">Florent Bréhard, Assia Mahboubi, and Damien Pous</span>
<span class="title">A Certificate-Based Approach to Formally Verified Approximations</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.8">10.4230/LIPIcs.ITP.2019.8</a>
</li>
<li>
<span class="authors">Chad E. Brown, Cezary Kaliszyk, and Karol Pąk</span>
<span class="title">Higher-Order Tarski Grothendieck as a Foundation for Formal Proof</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.9">10.4230/LIPIcs.ITP.2019.9</a>
</li>
<li>
<span class="authors">Matthias Brun and Dmitriy Traytel</span>
<span class="title">Generic Authenticated Data Structures, Formally</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.10">10.4230/LIPIcs.ITP.2019.10</a>
</li>
<li>
<span class="authors">Julian Brunner, Benedikt Seidl, and Salomon Sickert</span>
<span class="title">A Verified and Compositional Translation of LTL to Deterministic Rabin Automata</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.11">10.4230/LIPIcs.ITP.2019.11</a>
</li>
<li>
<span class="authors">Mario Carneiro</span>
<span class="title">Formalizing Computability Theory via Partial Recursive Functions</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.12">10.4230/LIPIcs.ITP.2019.12</a>
</li>
<li>
<span class="authors">Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry</span>
<span class="title">Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.13">10.4230/LIPIcs.ITP.2019.13</a>
</li>
<li>
<span class="authors">Łukasz Czajka</span>
<span class="title">First-Order Guarded Coinduction in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.14">10.4230/LIPIcs.ITP.2019.14</a>
</li>
<li>
<span class="authors">Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis</span>
<span class="title">Formalizing the Solution to the Cap Set Problem</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.15">10.4230/LIPIcs.ITP.2019.15</a>
</li>
<li>
<span class="authors">Manuel Eberl</span>
<span class="title">Nine Chapters of Analytic Number Theory in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.16">10.4230/LIPIcs.ITP.2019.16</a>
</li>
<li>
<span class="authors">Yannick Forster and Fabian Kunze</span>
<span class="title">A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.17">10.4230/LIPIcs.ITP.2019.17</a>
</li>
<li>
<span class="authors">Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier</span>
<span class="title">Formal Proof and Analysis of an Incremental Cycle Detection Algorithm</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.18">10.4230/LIPIcs.ITP.2019.18</a>
</li>
<li>
<span class="authors">Jesse Michael Han and Floris van Doorn</span>
<span class="title">A Formalization of Forcing and the Unprovability of the Continuum Hypothesis</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.19">10.4230/LIPIcs.ITP.2019.19</a>
</li>
<li>
<span class="authors">Maximilian P. L. Haslbeck and Peter Lammich</span>
<span class="title">Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.20">10.4230/LIPIcs.ITP.2019.20</a>
</li>
<li>
<span class="authors">Fabian Immler, Jonas Rädle, and Makarius Wenzel</span>
<span class="title">Virtualization of HOL4 in Isabelle</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.21">10.4230/LIPIcs.ITP.2019.21</a>
</li>
<li>
<span class="authors">Peter Lammich</span>
<span class="title">Generating Verified LLVM from Isabelle/HOL</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.22">10.4230/LIPIcs.ITP.2019.22</a>
</li>
<li>
<span class="authors">Peter Lammich and Tobias Nipkow</span>
<span class="title">Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.23">10.4230/LIPIcs.ITP.2019.23</a>
</li>
<li>
<span class="authors">Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux</span>
<span class="title">A Verified LL(1) Parser Generator</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.24">10.4230/LIPIcs.ITP.2019.24</a>
</li>
<li>
<span class="authors">Mihir Parang Mehta and William R. Cook</span>
<span class="title">Binary-Compatible Verification of Filesystems with ACL2</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.25">10.4230/LIPIcs.ITP.2019.25</a>
</li>
<li>
<span class="authors">Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman</span>
<span class="title">Ornaments for Proof Reuse in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.26">10.4230/LIPIcs.ITP.2019.26</a>
</li>
<li>
<span class="authors">Robert Sison and Toby Murray</span>
<span class="title">Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.27">10.4230/LIPIcs.ITP.2019.27</a>
</li>
<li>
<span class="authors">Florian Steinberg, Laurent Théry, and Holger Thies</span>
<span class="title">Quantitative Continuity and Computable Analysis in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.28">10.4230/LIPIcs.ITP.2019.28</a>
</li>
<li>
<span class="authors">Enrico Tassi</span>
<span class="title">Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.29">10.4230/LIPIcs.ITP.2019.29</a>
</li>
<li>
<span class="authors">Akihisa Yamada and Jérémy Dubut</span>
<span class="title">Complete Non-Orders and Fixed Points</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.30">10.4230/LIPIcs.ITP.2019.30</a>
</li>
<li>
<span class="authors">Minchao Wu and Rajeev Goré</span>
<span class="title">Verified Decision Procedures for Modal Logics</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.31">10.4230/LIPIcs.ITP.2019.31</a>
</li>
<li>
<span class="authors">Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen</span>
<span class="title">Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.32">10.4230/LIPIcs.ITP.2019.32</a>
</li>
<li>
<span class="authors">Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher</span>
<span class="title">The DPRM Theorem in Isabelle (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.33">10.4230/LIPIcs.ITP.2019.33</a>
</li>
<li>
<span class="authors">Jan Jakubův and Josef Urban</span>
<span class="title">Hammering Mizar by Learning Clause Guidance (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.34">10.4230/LIPIcs.ITP.2019.34</a>
</li>
<li>
<span class="authors">Cezary Kaliszyk and Karol Pąk</span>
<span class="title">Declarative Proof Translation (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.35">10.4230/LIPIcs.ITP.2019.35</a>
</li>
<li>
<span class="authors">Daniel E. Severín</span>
<span class="title">Formalization of the Domination Chain with Weighted Parameters (Short Paper)</span>
<a class="doi" href="https://doi.org/10.4230/LIPIcs.ITP.2019.36">10.4230/LIPIcs.ITP.2019.36</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