| 2019 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2019 | Verified Decision Procedures for Modal Logics. | Minchao Wu, Rajeev Gor |
| 2019 | Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. | Enrico Tassi |
| 2019 | Quantitative Continuity and Computable Analysis in Coq. | Florian Steinberg, Laurent Thry, Holger Thies |
| 2019 | Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. | Robert Sison, Toby Murray |
| 2019 | Formalization of the Domination Chain with Weighted Parameters (Short Paper). | Daniel E. Severn |
| 2019 | Ornaments for Proof Reuse in Coq. | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
| 2019 | Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. | Johannes man Pohjola, Henrik Rostedt, Magnus O. Myreen |
| 2019 | Binary-Compatible Verification of Filesystems with ACL2. | Mihir Parang Mehta, William R. Cook |
| 2019 | A Verified LL(1) Parser Generator. | Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux |
| 2019 | Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. | Peter Lammich, Tobias Nipkow |
| 2019 | Generating Verified LLVM from Isabelle/HOL. | Peter Lammich |
| 2019 | Declarative Proof Translation (Short Paper). | Cezary Kaliszyk, Karol Pak |
| 2019 | Hammering Mizar by Learning Clause Guidance (Short Paper). | Jan Jakubuv, Josef Urban |
| 2019 | Virtualization of HOL4 in Isabelle. | Fabian Immler, Jonas Rdle, Makarius Wenzel |
| 2019 | Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. | Maximilian P. L. Haslbeck, Peter Lammich |
| 2019 | A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. | Jesse Michael Han, Floris van Doorn |
| 2019 | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. | Armal Guneau, Jacques-Henri Jourdan, Arthur Charguraud, Franois Pottier |
| 2019 | Nine Chapters of Analytic Number Theory in Isabelle/HOL. | Manuel Eberl |
| 2019 | An Increasing Need for Formality (Invited Talk). | Martin Dixon |
| 2019 | Formalizing the Solution to the Cap Set Problem. | Sander R. Dahmen, Johannes Hlzl, Robert Y. Lewis |
| 2019 | Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. | Ran Chen, Cyril Cohen, Jean-Jacques Lvy, Stephan Merz, Laurent Thry |
| 2019 | Formalizing Computability Theory via Partial Recursive Functions. | Mario Carneiro |
| 2019 | What Makes a Mathematician Tick? (Invited Talk). | Kevin Buzzard |
| 2019 | Generic Authenticated Data Structures, Formally. | Matthias Brun, Dmitriy Traytel |