| Authors | Title | Paper | Talk |
|---|
| Jeremy Avigad, Johannes Hölzl and Luke Serafin | A formally verified proof of the Central Limit Theorem |  | Jul 13 08:45 |
| Holger Blasum, Oto Havle, Bruno Langenstein, Yakoub Nemouchi, Julien Schmaltz, Werner Stephan, Sergey Tverdyshev, Freek Verbeek and Burkhart Wolff | Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract) | | Jul 13 16:30 |
| Florian Haftmann, Andreas Lochbihler and Wolfgang Schreiner | Towards abstract and executable multivariate polynomials in Isabelle | | Jul 13 11:45 |
| Ondřej Kunčar and Andrei Popescu | From types to sets in Isabelle/HOL | | Jul 13 11:20 |
| Peter Lammich | The CAVA Automata Library | | Jul 13 10:55 |
| Andreas Lochbihler and Marc Züst | Programming TLS in Isabelle/HOL | | Jul 13 15:30 |
| Tobias Nipkow | Amortized Complexity Verified | | Jul 13 17:40 |
| Lars Noschinski | Towards Structured Proofs for Program Verification (Ongoing Work) | | Jul 13 17:20 |
| Lars Noschinski and Christoph Traut | Pattern-based Subterm Selection In Isabelle | | Jul 13 09:45 |
| Lorenz Panny, Jasmin Christian Blanchette and Dmitriy Traytel | Primitively (Co)recursive Definitions for Isabelle/HOL | | Jul 13 09:15 |
| Lawrence Paulson | Proving Gödel’s Incompleteness Theorems | | Jul 13 14:30 |
| Christine Rizkallah | A Simpl Shortest Path Checker Verification | | Jul 13 17:00 |
| Makarius Wenzel | Isabelle/jEdit NEWS | | Jul 13 15:00 |