ISABELLE PROGRAM
Thursday, August 11th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:10-10:30 Session 122: Isabelle 1
Chair:
Location: Ullmann 101
| 09:10 | Welcome |
| 09:20 | Auxiliary tools for Combinatorics on Words (abstract) PRESENTER: Stepan Holub |
| 09:35 | Transfer and reversal of lists (abstract) PRESENTER: Martin Raška |
| 10:00 | Oracle Integration of Floating-Point Solvers with Isabelle (abstract)   PRESENTER: Olle Torstensson |
10:30-11:00Coffee Break
11:00-12:30 Session 125G: Isabelle 2
Chair:
Location: Ullmann 101
| 11:00 | A Verified Implementation of B-trees in Isabelle/HOL (abstract) PRESENTER: Niels Mündler |
| 11:30 | On Axiomatic Systems for Classical Propositional Logic (abstract) PRESENTER: Jørgen Villadsen |
| 11:50 | On Termination for Hybrid Tableaux (abstract) |
| 12:10 | Lessons of Teaching Formal Methods with Isabelle (abstract) PRESENTER: Frederik Krogsdal Jacobsen |
12:30-14:00Lunch Break
Lunches will be held in Taub hall and in The Grand Water Research Institute.
14:00-15:30 Session 127G: Isabelle 3
Chair:
Location: Ullmann 101
| 14:00 | Isabelle/VSCode and Electron/Node.js as emerging Isabelle technologies (abstract) |
| 14:30 | Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode (abstract) PRESENTER: Bernhard Stöger |
| 15:00 | A Linter for Isabelle: Implementation and Evaluation (abstract) PRESENTER: Fabian Huch |
15:30-16:00Coffee Break
16:00-17:30 Session 131E: Isabelle 4
Chair:
Location: Ullmann 101
| 16:00 | Gale-Shapley Verified (abstract) |
| 16:30 | From P != NP to monotone circuits of super-polynomial size (abstract) |
| 17:00 | Automating Kantian Ethics in Isabelle: A Case Study (abstract) |
18:00-19:30Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event