LIPIcs, Volume 141, ITP 2019

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