Program

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 Points
Akihisa Yamada, Jérémy Dubut

11:00–11:30

Formalizing computability theory via partial recursive functions
Mario Carneiro

11:30–12:00

A formalization of forcing and the consistency of the failure of the continuum hypothesis
Jesse Han, Floris van Doorn

12:00–13:30

Lunch

Session 3

13:30–14:00

Generating Verified LLVM from Isabelle/HOL
Peter Lammich

14:00–14:30

Virtualization of HOL4 in Isabelle
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)
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
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
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
Enrico Tassi

11:00–11:30

Data types as quotients of polynomial functors
Jeremy Avigad, Mario Carneiro, Simon Hudon

11:30–12:00

Ornaments for Proof Reuse in Coq
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
Salomon Sickert, Julian Brunner, Benedikt Seidl

14:00–14:30

Verified Decision Procedures for Modal Logics
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
Florent Bréhard, Assia Mahboubi, Damien Pous

16:00–16:30

Primitive Floats in Coq
Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux

16:30–17:00

Quantitative continuity and computable analysis in Coq
Florian Steinberg, Laurent Thery, Holger Thies

 

 

Wednesday 11 September 2019

Session 9

09:00–9:30

Generic Authenticated Data Structures, Formally
Matthias Brun, Dmitriy Traytel

09:30–10:00

Verifying that a compiler preserves concurrent value-dependent information-flow security
Robert Sison, Toby Murray

10:00–10:30

Break

Session 10

10:30–11:00

First-order guarded coinduction in Coq
Lukasz Czajka

11:00–11:30

A Verified Compositional Algorithm for AI Planning
Mohammad 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 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)
Marco David, Jonas Bayer, Abhik Pal, Benedikt Stock

11:00–11:30

Formalizing the Solution to the Cap Set Problem
Sander Dahmen, Johannes Hölzl, Robert Y. Lewis

11:30–12:00

Nine Chapters of Analytic Number Theory in Isabelle/HOL
Manuel Eberl

12:00–13:30

Lunch

Session 13

13:30–14:00

Binary-compatible verification of filesystems with ACL2
Mihir Mehta, William Cook

14:00–14:30

Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs
Johannes Aman Pohjola, Henrik Rostedt, Magnus O. Myreen

14:30–15:00

A Verified LL(1) Parser Generator
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
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
Yannick Forster, Fabian Kunze

Comments are closed.