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