The program is subject to change.
| Monday 9 September 2019 | ||
|---|---|---|
| 08:00–09:00 | Registration | |
| Session 1 | ||
| 09:00–10:00 | Invited talk: What makes a mathematician tick? (slides) Kevin Buzzard | |
| 10:00–10:30 | Break | |
| Session 2 | ||
| 10:30–11:00 | Complete Non-Orders and Fixed Points (slides) Akihisa Yamada, Jérémy Dubut | |
| 11:00–11:30 | Formalizing computability theory via partial recursive functions (slides) Mario Carneiro | |
| 11:30–12:00 | A formalization of forcing and the consistency of the failure of the continuum hypothesis (slides) Jesse Han, Floris van Doorn | |
| 12:00–13:30 | Lunch | |
| Session 3 | ||
| 13:30–14:00 | Generating Verified LLVM from Isabelle/HOL (slides) Peter Lammich | |
| 14:00–14:30 | Virtualization of HOL4 in Isabelle (slides) Fabian Immler, Jonas Rädle, Makarius Wenzel | |
| 14:30–14:45 | Declarative Proof Translation (short paper) Cezary Kaliszyk, Karol Pak | |
| 14:45–15:00 | Hammering Mizar by Learning Clause Guidance (short paper) (slides) Jan Jakubuv, Josef Urban | |
| 15:00–15:30 | Break | |
| Session 4 | ||
| 15:30–16:00 | Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra (slides) Peter Lammich, Tobias Nipkow | |
| 16:00–16:30 | Formal Proof of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq, and Isabelle Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery | |
| 16:30–17:00 | Proving tree algorithms for succinct data structures (slides) Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka | |
| Tuesday 10 September 2019 | ||
| Session 5 | ||
| 09:00–10:00 | Invited talk: An Increasing Need for Formality Martin Dixon | |
| 10:00–10:30 | Break | |
| Session 6 | ||
| 10:30–11:00 | Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq (slides) Enrico Tassi | |
| 11:00–11:30 | Data types as quotients of polynomial functors (slides) Jeremy Avigad, Mario Carneiro, Simon Hudon | |
| 11:30–12:00 | Ornaments for Proof Reuse in Coq (slides) Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman | |
| 12:00–13:30 | Lunch | |
| Session 7 | ||
| 13:30–14:00 | A Verified and Compositional Translation of LTL to Deterministic Rabin Automata (slides) Salomon Sickert, Julian Brunner, Benedikt Seidl | |
| 14:00–14:30 | Verified Decision Procedures for Modal Logics (slides) Minchao Wu, Rajeev Goré | |
| 14:30–15:00 | Higher-order Tarski Grothendieck as a Foundation for Formal Proof Chad Brown, Cezary Kaliszyk, Karol Pak | |
| 15:00–15:30 | Break | |
| Session 8 | ||
| 15:30–16:00 | A certificate-based approach to formally verified approximations (slides) Florent Bréhard, Assia Mahboubi, Damien Pous | |
| 16:00–16:30 | Primitive Floats in Coq (slides) Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux | |
| 16:30–17:00 | Quantitative continuity and computable analysis in Coq (slides) Florian Steinberg, Laurent Thery, Holger Thies | |
| Wednesday 11 September 2019 | ||
| Session 9 | ||
| 09:00–9:30 | Generic Authenticated Data Structures, Formally (slides) Matthias Brun, Dmitriy Traytel | |
| 09:30–10:00 | Verifying that a compiler preserves concurrent value-dependent information-flow security (slides) Robert Sison, Toby Murray | |
| 10:00–10:30 | Break | |
| Session 10 | ||
| 10:30–11:00 | First-order guarded coinduction in Coq (slides) Lukasz Czajka | |
| 11:00–11:30 | A Verified Compositional Algorithm for AI Planning (slides) Mohammad Abdulaziz, Charles Gretton, Michael Norrish | |
| 11:30–12:15 | Business Meeting (slides) | |
| 17:15–20:00 | Banquet and River Cruise aboard the Willamette Star | |
| Thursday 12 September 2019 | ||
| Session 11 | ||
| 09:00–10:00 | Invited talk: A Million Lines of Proof About a Moving Target June Andronick | |
| 10:00–10:30 | Break | |
| Session 12 | ||
| 10:30–10:45 | Formalization of the Domination Chain with Weighted Parameters (short paper) Daniel Severin | |
| 10:45–11:00 | The DPRM theorem in Isabelle (short paper) (slides) Marco David, Jonas Bayer, Abhik Pal, Benedikt Stock | |
| 11:00–11:30 | Formalizing the Solution to the Cap Set Problem (slides) Sander Dahmen, Johannes Hölzl, Robert Y. Lewis | |
| 11:30–12:00 | Nine Chapters of Analytic Number Theory in Isabelle/HOL (slides) Manuel Eberl | |
| 12:00–13:30 | Lunch | |
| Session 13 | ||
| 13:30–14:00 | Binary-compatible verification of filesystems with ACL2 (slides) Mihir Mehta, William Cook | |
| 14:00–14:30 | Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs (slides) Johannes Aman Pohjola, Henrik Rostedt, Magnus O. Myreen | |
| 14:30–15:00 | A Verified LL(1) Parser Generator (slides) Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux | |
| 15:00–15:30 | Break | |
| Session 14 | ||
| 15:30–16:00 | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm (slides) Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier | |
| 16:00–16:30 | Refinement with Time – Refining the Run-time of Algorithms in Isabelle/HOL Maximilian Paul Louis Haslbeck, Peter Lammich | |
| 16:30–17:00 | A certifying extraction with time bounds from Coq to call-by-value λ-calculus (slides) Yannick Forster, Fabian Kunze | |