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?Kevin Buzzard | |

10:00–10:30 | Break | |

Session 2
| ||

10:30–11:00 | Complete Non-Orders and Fixed PointsAkihisa Yamada, Jérémy Dubut | |

11:00–11:30 | Formalizing computability theory via partial recursive functionsMario Carneiro | |

11:30–12:00 | A formalization of forcing and the consistency of the failure of the continuum hypothesisJesse Han, Floris van Doorn | |

12:00–13:30 | Lunch | |

Session 3
| ||

13:30–14:00 | Generating Verified LLVM from Isabelle/HOLPeter Lammich | |

14:00–14:30 | Virtualization of HOL4 in IsabelleFabian 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)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 DijkstraPeter 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 structuresReynald 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 CoqEnrico Tassi | |

11:00–11:30 | Data types as quotients of polynomial functorsJeremy Avigad, Mario Carneiro, Simon Hudon | |

11:30–12:00 | Ornaments for Proof Reuse in CoqTalia 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 AutomataSalomon Sickert, Julian Brunner, Benedikt Seidl | |

14:00–14:30 | Verified Decision Procedures for Modal LogicsMinchao 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 approximationsFlorent Bréhard, Assia Mahboubi, Damien Pous | |

16:00–16:30 | Primitive Floats in CoqGuillaume Bertholon, Érik Martin-Dorel, Pierre Roux | |

16:30–17:00 | Quantitative continuity and computable analysis in CoqFlorian Steinberg, Laurent Thery, Holger Thies | |

Wednesday 11 September 2019 | ||

Session 9
| ||

09:00–9:30 | Generic Authenticated Data Structures, FormallyMatthias Brun, Dmitriy Traytel | |

09:30–10:00 | Verifying that a compiler preserves concurrent value-dependent information-flow securityRobert Sison, Toby Murray | |

10:00–10:30 | Break | |

Session 10
| ||

10:30–11:00 | First-order guarded coinduction in CoqLukasz Czajka | |

11:00–11:30 | A Verified Compositional Algorithm for AI PlanningMohammad Abdulaziz, Charles Gretton, Michael Norrish | |

11:30–12:15 | Business Meeting | |

17:00–20:00 | Banquet 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)Marco David, Jonas Bayer, Abhik Pal, Benedikt Stock | |

11:00–11:30 | Formalizing the Solution to the Cap Set ProblemSander Dahmen, Johannes Hölzl, Robert Y. Lewis | |

11:30–12:00 | Nine Chapters of Analytic Number Theory in Isabelle/HOLManuel Eberl | |

12:00–13:30 | Lunch | |

Session 13
| ||

13:30–14:00 | Binary-compatible verification of filesystems with ACL2Mihir Mehta, William Cook | |

14:00–14:30 | Characteristic Formulae for Liveness Properties of Non-terminating CakeML ProgramsJohannes Aman Pohjola, Henrik Rostedt, Magnus O. Myreen | |

14:30–15:00 | A Verified LL(1) Parser GeneratorSam 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 AlgorithmArmaë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 λ-calculusYannick Forster, Fabian Kunze |