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 IsabelleRan 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 FormalityMartin 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 ProofChad 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 TargetJune 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/HOLMaximilian 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 |