FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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

10:30-11:00Coffee Break
11:00-12:00 Session 45C: ITP Invited Talk: John Harrison
Location: Blavatnik LT1
11:00
Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification (abstract)
12:00-12:30 Session 46
Location: Blavatnik LT1
12:00
Efficient Mendler-Style Lambda-Encodings in Cedille (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 47C
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 49C
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).

Tuesday, July 10th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:00 Session 50C: ITP Invited Talk: Dan Grayson
Location: Blavatnik LT1
09:00
Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics (abstract)
10:00-10:30 Session 51A
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 52C
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 53C
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 55C
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 56: 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).

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 57D
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 61C
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
15:30-16:00Coffee Break
16:00-18:00 Session 64C
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).

Thursday, July 12th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 67C
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 71C
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
15:00-15:30 Session 74B
Location: Blavatnik LT1
15:00
ProofWatch: Watchlist Guidance for Large Theories in E (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 75B
Location: Blavatnik LT1
16:00
Verified Tail Bounds for Randomized Programs (abstract)
16:30
Verified Analysis of Random Binary Tree Structures (abstract)