Portal - ITP 2019

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

Haslbeck, Maximilian P. L.

Jourdan, Jacques-Henri

Åman Pohjola, Johannes

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

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