ITP 2019 September 9-12, 2019, Portland, OR, USA

10th International Conference on Interactive Theorem Proving (ITP 2019)



John Harrison and John O'Leary and Andrew Tolmach (Eds.)
ISBN 978-3-95977-122-1, LIPICS Vol. 141 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 16 MB)
Search Publication Server

Authors
  • Abdulaziz, Mohammad
  • Affeldt, Reynald
  • Åman Pohjola, Johannes
  • Andronick, June
  • Avigad, Jeremy
  • Bayer, Jonas
  • Bertholon, Guillaume
  • Bréhard, Florent
  • Brown, Chad E.
  • Brun, Matthias
  • Brunner, Julian
  • Buzzard, Kevin
  • Carneiro, Mario
  • Casinghino, Chris
  • Charguéraud, Arthur
  • Chen, Ran
  • Cohen, Cyril
  • Cook, William R.
  • Czajka, Lukasz
  • Dahmen, Sander R.
  • David, Marco
  • Dixon, Martin
  • Dubut, Jérémy
  • Eberl, Manuel
  • Fisher, Kathleen
  • Forster, Yannick
  • Garrigue, Jacques
  • Goré, Rajeev
  • Gretton, Charles
  • Grossman, Dan
  • Guéneau, Armaël
  • Han, Jesse Michael
  • Harrison, John
  • Haslbeck, Maximilian P. L.
  • Hölzl, Johannes
  • Hudon, Simon
  • Immler, Fabian
  • Jakubuv, Jan
  • Jourdan, Jacques-Henri
  • Kaliszyk, Cezary
  • Kunze, Fabian
  • Lammich, Peter
  • Lasser, Sam
  • Leo, John
  • Lévy, Jean-Jacques
  • Lewis, Robert Y.
  • Mahboubi, Assia
  • Martin-Dorel, Érik
  • Mehta, Mihir Parang
  • Merz, Stephan
  • Murray, Toby
  • Myreen, Magnus O.
  • Nipkow, Tobias
  • Norrish, Michael
  • O'Leary, John
  • Pak, Karol
  • Pal, Abhik
  • Pottier, François
  • Pous, Damien
  • Qi, Xuanrui
  • Rädle, Jonas
  • Ringer, Talia
  • Rostedt, Henrik
  • Roux, Cody
  • Roux, Pierre
  • Schleicher, Dierk
  • Seidl, Benedikt
  • Severín, Daniel E.
  • Sickert, Salomon
  • Sison, Robert
  • Steinberg, Florian
  • Stock, Benedikt
  • Tanaka, Kazunari
  • Tassi, Enrico
  • Théry, Laurent
  • Thies, Holger
  • Tolmach, Andrew
  • Traytel, Dmitriy
  • Urban, Josef
  • van Doorn, Floris
  • Wenzel, Makarius
  • Wu, Minchao
  • Yamada, Akihisa
  • Yazdani, Nathaniel
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Harrison, John ; O'Leary, John ; Tolmach, Andrew

    Abstract | Document (301 KB) | BibTeX

    A Million Lines of Proof About a Moving Target (Invited Talk)
    Authors: Andronick, June

    Abstract | Document (158 KB) | BibTeX

    What Makes a Mathematician Tick? (Invited Talk)
    Authors: Buzzard, Kevin

    Abstract | Document (154 KB) | BibTeX

    An Increasing Need for Formality (Invited Talk)
    Authors: Dixon, Martin

    Abstract | Document (155 KB) | BibTeX

    A Verified Compositional Algorithm for AI Planning
    Authors: Abdulaziz, Mohammad ; Gretton, Charles ; Norrish, Michael

    Abstract | Document (556 KB) | BibTeX

    Proving Tree Algorithms for Succinct Data Structures
    Authors: Affeldt, Reynald ; Garrigue, Jacques ; Qi, Xuanrui ; Tanaka, Kazunari

    Abstract | Document (510 KB) | BibTeX

    Data Types as Quotients of Polynomial Functors
    Authors: Avigad, Jeremy ; Carneiro, Mario ; Hudon, Simon

    Abstract | Document (502 KB) | BibTeX

    Primitive Floats in Coq
    Authors: Bertholon, Guillaume ; Martin-Dorel, Érik ; Roux, Pierre

    Abstract | Document (622 KB) | BibTeX

    A Certificate-Based Approach to Formally Verified Approximations
    Authors: Bréhard, Florent ; Mahboubi, Assia ; Pous, Damien

    Abstract | Document (556 KB) | BibTeX

    Higher-Order Tarski Grothendieck as a Foundation for Formal Proof
    Authors: Brown, Chad E. ; Kaliszyk, Cezary ; Pak, Karol

    Abstract | Document (519 KB) | BibTeX

    Generic Authenticated Data Structures, Formally
    Authors: Brun, Matthias ; Traytel, Dmitriy

    Abstract | Document (506 KB) | BibTeX

    A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
    Authors: Brunner, Julian ; Seidl, Benedikt ; Sickert, Salomon

    Abstract | Document (605 KB) | BibTeX

    Formalizing Computability Theory via Partial Recursive Functions
    Authors: Carneiro, Mario

    Abstract | Document (482 KB) | BibTeX

    Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
    Authors: Chen, Ran ; Cohen, Cyril ; Lévy, Jean-Jacques ; Merz, Stephan ; Théry, Laurent

    Abstract | Document (567 KB) | BibTeX

    First-Order Guarded Coinduction in Coq
    Authors: Czajka, Lukasz

    Abstract | Document (489 KB) | BibTeX

    Formalizing the Solution to the Cap Set Problem
    Authors: Dahmen, Sander R. ; Hölzl, Johannes ; Lewis, Robert Y.

    Abstract | Document (523 KB) | BibTeX

    Nine Chapters of Analytic Number Theory in Isabelle/HOL
    Authors: Eberl, Manuel

    Abstract | Document (561 KB) | BibTeX

    A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus
    Authors: Forster, Yannick ; Kunze, Fabian

    Abstract | Document (654 KB) | BibTeX

    Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
    Authors: Guéneau, Armaël ; Jourdan, Jacques-Henri ; Charguéraud, Arthur ; Pottier, François

    Abstract | Document (524 KB) | BibTeX

    A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
    Authors: Han, Jesse Michael ; van Doorn, Floris

    Abstract | Document (663 KB) | BibTeX

    Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL
    Authors: Haslbeck, Maximilian P. L. ; Lammich, Peter

    Abstract | Document (507 KB) | BibTeX

    Virtualization of HOL4 in Isabelle
    Authors: Immler, Fabian ; Rädle, Jonas ; Wenzel, Makarius

    Abstract | Document (665 KB) | BibTeX

    Generating Verified LLVM from Isabelle/HOL
    Authors: Lammich, Peter

    Abstract | Document (518 KB) | BibTeX

    Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
    Authors: Lammich, Peter ; Nipkow, Tobias

    Abstract | Document (441 KB) | BibTeX

    A Verified LL(1) Parser Generator
    Authors: Lasser, Sam ; Casinghino, Chris ; Fisher, Kathleen ; Roux, Cody

    Abstract | Document (511 KB) | BibTeX

    Binary-Compatible Verification of Filesystems with ACL2
    Authors: Mehta, Mihir Parang ; Cook, William R.

    Abstract | Document (492 KB) | BibTeX

    Ornaments for Proof Reuse in Coq
    Authors: Ringer, Talia ; Yazdani, Nathaniel ; Leo, John ; Grossman, Dan

    Abstract | Document (507 KB) | BibTeX

    Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security
    Authors: Sison, Robert ; Murray, Toby

    Abstract | Document (626 KB) | BibTeX

    Quantitative Continuity and Computable Analysis in Coq
    Authors: Steinberg, Florian ; Théry, Laurent ; Thies, Holger

    Abstract | Document (612 KB) | BibTeX

    Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq
    Authors: Tassi, Enrico

    Abstract | Document (396 KB) | BibTeX

    Complete Non-Orders and Fixed Points
    Authors: Yamada, Akihisa ; Dubut, Jérémy

    Abstract | Document (464 KB) | BibTeX

    Verified Decision Procedures for Modal Logics
    Authors: Wu, Minchao ; Goré, Rajeev

    Abstract | Document (499 KB) | BibTeX

    Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs
    Authors: Åman Pohjola, Johannes ; Rostedt, Henrik ; Myreen, Magnus O.

    Abstract | Document (529 KB) | BibTeX

    The DPRM Theorem in Isabelle (Short Paper)
    Authors: Bayer, Jonas ; David, Marco ; Pal, Abhik ; Stock, Benedikt ; Schleicher, Dierk

    Abstract | Document (428 KB) | BibTeX

    Hammering Mizar by Learning Clause Guidance (Short Paper)
    Authors: Jakubuv, Jan ; Urban, Josef

    Abstract | Document (354 KB) | BibTeX

    Declarative Proof Translation (Short Paper)
    Authors: Kaliszyk, Cezary ; Pak, Karol

    Abstract | Document (530 KB) | BibTeX

    Formalization of the Domination Chain with Weighted Parameters (Short Paper)
    Authors: Severín, Daniel E.

    Abstract | Document (395 KB) | BibTeX

    		  



    DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI