| 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 |
| 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 |