ITP PROGRAM
Days: Monday, July 9th Tuesday, July 10th Wednesday, July 11th Thursday, July 12th
Monday, July 9th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 46: FLoC Plenary Lecture: Peter O'Hearn
Chair:
Location: Maths LT1
| 09:00 | Continuous Reasoning: Scaling the Impact of Formal Methods (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 47C: ITP Invited Talk: John Harrison
Chair:
Location: Blavatnik LT1
| 11:00 | Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification (abstract)  |
12:00-12:30 Session 48
Chair:
Location: Blavatnik LT1
| 12:00 | Efficient Mendler-Style Lambda-Encodings in Cedille (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 49C
Chair:
Location: Blavatnik LT1
| 14:00 | Formalizing Implicative Algebras in Coq (abstract) |
| 14:30 | Software Tool Support for Modular Reasoning in Modal Logics of Actions (abstract) |
| 15:00 | The Coinductive Formulation of Common Knowledge (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 51C
Chair:
Location: Blavatnik LT1
| 16:00 | Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (abstract) |
| 16:30 | Boosting the Reuse of Formal Specifications (abstract) |
| 17:00 | Formalization of a Polymorphic Subtyping Algorithm (abstract) |
| 17:30 | A Formal Equational Theory for Call-by-Push-Value (abstract) |
19:00-21:30 FLoC reception at Ashmolean Museum
FLoC reception at Ashmolean Museum. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Ashmolean Museum
Tuesday, July 10th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:00 Session 52C: ITP Invited Talk: Dan Grayson
Chair:
Location: Blavatnik LT1
| 09:00 | Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics (abstract) |
10:00-10:30 Session 53A
Chair:
Location: Blavatnik LT1
| 10:00 | CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math” (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 54C
Chair:
Location: Blavatnik LT1
| 11:00 | A Formalization of the LLL Basis Reduction Algorithm (abstract) |
| 11:30 | A Formally Verified Solver for Homogeneous Linear Diophantine Equations (abstract) |
| 12:00 | A Coq Tactic for Equality Learning in Linear Arithmetic (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 55C
Chair:
Location: Blavatnik LT1
| 14:00 | Backwards and Forwards with Separation Logic (abstract) |
| 14:30 | Reification by Parametricity (abstract) |
| 15:00 | A Coq Formalisation of SQL’S Execution Engines (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 58B
Chair:
Location: Blavatnik LT1
| 16:00 | An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (abstract) |
| 16:30 | Towards Certified Meta-Programming with Typed Template-Coq (abstract) |
17:00-18:30 Session 59: FLoC Public Lecture: Stuart Russell
Doors open at 4:30 pm; please be seated by 4:50 pm (attendance is free of charge and all are welcome; please register).
Chair:
Location: Sheldonian Theatre
| 17:00 | Unifying Logic and Probability: the BLOG Language (abstract) |
Wednesday, July 11th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 60D
Chair:
Location: Blavatnik LT1
| 09:00 | Program Verification in the Presence of Cached Address Translation (abstract) |
| 09:30 | Physical Addressing on Real Hardware in Isabelle/HOL (abstract) |
| 10:00 | Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 64C
Chair:
Location: Blavatnik LT1
| 11:00 | Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (abstract) |
| 11:30 | HOL Light QE (abstract) |
| 12:00 | Tactics and Certificates in Meta Dedukti (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 66A: FLoC Keynote Lecture: Shafi Goldwasser
Chair:
Location: Maths LT1
| 14:00 | Pseudo deterministic algorithms and proofs (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 67C
Chair:
Location: Blavatnik LT1
| 16:00 | Towards Formal Foundations for Game Theory (Short Paper) (abstract) |
| 16:20 | MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (abstract) |
| 16:40 | Towards Verified Handwritten Calculational Proofs (Short Paper) (abstract) |
| 17:00 | Formalizing Ring Theory in PVS (Short Paper) (abstract) |
| 17:20 | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) (abstract) |
19:00-21:30 FLoC banquet at Examination Schools
FLoC banquet at Examination Schools. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Examination Schools
Thursday, July 12th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 70C
Chair:
Location: Blavatnik LT1
| 09:00 | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (abstract) |
| 09:30 | Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (abstract) |
| 10:00 | Verification of PCP-Related Computational Reductions in Coq (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 74C
Chair:
Location: Blavatnik LT1
| 11:00 | Verified Memoization and Dynamic Programming (abstract) |
| 11:30 | Fast Machine Words in Isabelle/HOL (abstract) |
| 12:00 | Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (abstract) |
12:30-14:00Lunch Break
14:00-15:00 Session 76D: ITP Invited Talk: Jean-Christophe Filliâtre
Chair:
Location: Blavatnik LT1
| 14:00 | Deductive Program Verification (abstract) |
15:00-15:30 Session 77B
Chair:
Location: Blavatnik LT1
| 15:00 | ProofWatch: Watchlist Guidance for Large Theories in E (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 78B
Chair:
Location: Blavatnik LT1
| 16:00 | Verified Tail Bounds for Randomized Programs (abstract) |
| 16:30 | Verified Analysis of Random Binary Tree Structures (abstract) |