ISABELLE PROGRAM
Friday, July 13th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:30-10:30 Session 84A: Isabelle 1
Chair:
Location: Blavatnik LT1
| 09:30 | A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (abstract)  |
| 10:00 | Lazy Algebraic Types in Isabelle/HOL (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 86E: Isabelle 2
Chair:
Location: Blavatnik LT1
| 11:00 | Formal Verification of Bounds for the LLL Basis Reduction Algorithm (abstract) |
| 11:30 | Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (abstract)  |
| 12:00 | Further Scaling of Isabelle Technology (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 87N: UITP 3/ Isabelle 3 Joint Session (joint with UITP)
Chair:
Location: Blavatnik Seminar Room 4
| 14:00 | Isabelle/PIDE after 10 years of development (abstract) |
| 14:30 | Text-Orientated Formal Mathematics (abstract) |
| 15:00 | Drawing Trees (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 88C: Isabelle 4
Chair:
Location: Blavatnik LT1
| 16:00 | Substitutionless First-Order Logic: A Formal Soundness Proof (abstract) |
| 16:15 | The remote_build Tool (abstract) |
| 16:30 | PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (abstract) |
| 17:00 | Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (abstract) |
19:00-21:30 Workshops dinner at Keble College
Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).
Location: Keble College