10.1145/acmotherconferences
ACM Other Conferences
0000000
10.5555/0000000
Proceedings of the 10th International Conference on Interactive Theorem Proving (ITP 2019)
ITP 2019
Harrison
John
Amazon AWS, Portland, OR, USA
jrh013@gmail.com
Editor
O'Leary
John
Intel Corporation
john.w.oleary@intel.com
Editor
Tolmach
Andrew
Portland State University, Portland, OR, USA
tolmach@pdx.edu
Editor
05
09
2019
9783959771221
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
PUB7509
Germany
2019
09
09
2019
12
09
2019
ITP 2019
ITP 2019
A Million Lines of Proof About a Moving Target (Invited Talk)
10.4230/LIPIcs.ITP.2019.1
1
What Makes a Mathematician Tick? (Invited Talk)
10.4230/LIPIcs.ITP.2019.2
2
An Increasing Need for Formality (Invited Talk)
10.4230/LIPIcs.ITP.2019.3
3
A Verified Compositional Algorithm for AI Planning
10.4230/LIPIcs.ITP.2019.4
4
Proving Tree Algorithms for Succinct Data Structures
10.4230/LIPIcs.ITP.2019.5
5
Data Types as Quotients of Polynomial Functors
10.4230/LIPIcs.ITP.2019.6
6
Primitive Floats in Coq
10.4230/LIPIcs.ITP.2019.7
7
A Certificate-Based Approach to Formally Verified Approximations
10.4230/LIPIcs.ITP.2019.8
8
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof
10.4230/LIPIcs.ITP.2019.9
9
Generic Authenticated Data Structures, Formally
10.4230/LIPIcs.ITP.2019.10
10
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
10.4230/LIPIcs.ITP.2019.11
11
Formalizing Computability Theory via Partial Recursive Functions
10.4230/LIPIcs.ITP.2019.12
12
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle
10.4230/LIPIcs.ITP.2019.13
13
First-Order Guarded Coinduction in Coq
10.4230/LIPIcs.ITP.2019.14
14
Formalizing the Solution to the Cap Set Problem
10.4230/LIPIcs.ITP.2019.15
15
Nine Chapters of Analytic Number Theory in Isabelle/HOL
10.4230/LIPIcs.ITP.2019.16
16
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus
10.4230/LIPIcs.ITP.2019.17
17
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
10.4230/LIPIcs.ITP.2019.18
18
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
10.4230/LIPIcs.ITP.2019.19
19
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL
10.4230/LIPIcs.ITP.2019.20
20
Virtualization of HOL4 in Isabelle
10.4230/LIPIcs.ITP.2019.21
21
Generating Verified LLVM from Isabelle/HOL
10.4230/LIPIcs.ITP.2019.22
22
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
10.4230/LIPIcs.ITP.2019.23
23
A Verified LL(1) Parser Generator
10.4230/LIPIcs.ITP.2019.24
24
Binary-Compatible Verification of Filesystems with ACL2
10.4230/LIPIcs.ITP.2019.25
25
Ornaments for Proof Reuse in Coq
10.4230/LIPIcs.ITP.2019.26
26
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security
10.4230/LIPIcs.ITP.2019.27
27
Quantitative Continuity and Computable Analysis in Coq
10.4230/LIPIcs.ITP.2019.28
28
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq
10.4230/LIPIcs.ITP.2019.29
29
Complete Non-Orders and Fixed Points
10.4230/LIPIcs.ITP.2019.30
30
Verified Decision Procedures for Modal Logics
10.4230/LIPIcs.ITP.2019.31
31
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs
10.4230/LIPIcs.ITP.2019.32
32
The DPRM Theorem in Isabelle (Short Paper)
10.4230/LIPIcs.ITP.2019.33
33
Hammering Mizar by Learning Clause Guidance (Short Paper)
10.4230/LIPIcs.ITP.2019.34
34
Declarative Proof Translation (Short Paper)
10.4230/LIPIcs.ITP.2019.35
35
Formalization of the Domination Chain with Weighted Parameters (Short Paper)
10.4230/LIPIcs.ITP.2019.36
36