## Conference Program

### Monday, January 16th

09:00 Invited talk | |

- | Porting the HOL Light analysis library: Some lessons [Slides/PDF] |

Larry Paulson | |

10:30 Algorithm and library verification | |

- | Verifying a hash table and its iterators in higher-order separation logic |

François Pottier | |

- | A Formalization of the Berlekamp-Zassenhaus factorization algorithm |

Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada | |

- | Formal foundations of 3D geometry to model robot manipulators |

Reynald Affeldt and Cyril Cohen | |

14:00 Automated proof and its formal verification | |

- | BliStrTune: Hierarchical invention of theorem proving strategies |

Jan Jakubuv and Josef Urban | |

- | Automatic cyclic termination proofs for recursive procedures in separation logic |

Reuben Rowe and James Brotherston | |

- | Formalization of Karp-Miller tree construction on Petri nets |

Mitsuharu Yamamoto, Shogo Sekine and Saki Matsumoto | |

16:00 Formalized Mathematics with numerical computations | |

- | A Coq formal proof of the Lax–Milgram theorem |

Sylvie Boldo, François Clement, Florian Faissole, Vincent Martin and Micaela Mayero | |

- | A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations |

Érik Martin-Dorel and Pierre Roux | |

- | Markov processes in Isabelle/HOL |

Johannes Hölzl | |

- | Formalising real numbers in homotopy type theory |

Gaetan Gilbert |

### Tuesday, January 17th

09:00 Invited talk | |

- | Mechanized verification of preemptive OS kernels [Slides/PDF] |

Xinyu Feng | |

10:30 Verified programming tools | |

- | Verified compilation of CakeML to multiple machine-code targets |

Anthony Fox, Magnus O. Myreen, Yong Kiam Tan and Ramana Kumar | |

- | Complx: a verification framework for concurrent imperative programs |

Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong | |

- | Verifying dynamic race detection |

William Mansky, Yuanfeng Peng, Steve Zdancewic and Joseph Devietti | |

14:00 Homotopy Type Theory | |

- | The HoTT library: A formalization of homotopy type theory in Coq |

Andrej Bauer, Jason Gross, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu Sozeau and Bas Spitters | |

- | Lifting proof-relevant unification to higher dimensions |

Jesper Cockx and Dominique Devriese | |

- | The Next 700 syntactical models of type theory |

Simon Boulier, Pierre-Marie Pédrot and Nicolas Tabareau | |

16:00 Formal verification of programming language foundations | |

- | Type-and-scope safe programs and their proofs |

Guillaume Allais, James Chapman, Conor McBride and James McKinna | |

- | Formally verified differential dynamic logic |

Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Voelp and Andre Platzer | |

- | Equivalence of System F and λ2 in Coq based on context morphism lemmas |

Jonas Kaiser, Tobias Tebbi and Gert Smolka |