Sunday, July 11th
Sunday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Session 1
Chair: Matt Kaufmann [NOTE: A copy of the full program, with links to slides as well as to the agenda and minutes of the business meeting, may be found HERE.]
Location: AT LT5
| 09:00 | Norbert Schirmer and Ernie Cohen From Total Store Order to Sequential Consistency: A Practical Reduction Theorem |
| 09:30 | Freek Verbeek and Julien Schmaltz Proof Pearl: A formal proof of Duato's condition for deadlock-free adaptive networks |
10:30‑12:30 Session 2
Chair: David Pichardie
Location: AT LT5
| 10:30 | Ramana Kumar and Michael Norrish (Nominal) Unification by Recursive Descent with Triangular Substitutions |
| 11:00 | Jean-François Dufourd and Yves Bertot Formal study of plane Delaunay triangulation |
| 11:30 | Sylvie Boldo, François Clément, Jean-Christophe Filliatre, Micaela Mayero, Guillaume Melquiond and Pierre Weis Formal Proof of a Wave Equation Resolution Scheme: the Method Error |
| 12:00 | Anthony Fox and Magnus Myreen A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture |
14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
Location: George Square Lecture Theatre
| 14:00 | David Harel (Weizmann Institute of Science) Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's. |
| 14:30 | Gordon Plotkin (University of Edinburgh) Robin Milner, a Craftsman of Tools for the Mind. |
15:30‑17:00 Session 3
Chair: Cesar Munoz
Location: AT LT5
| 15:30 | Brian Huffman and Christian Urban Proof Pearl: A New Foundation for Nominal Isabelle |
| 16:00 | John Cowles and Ruben Gamboa Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure |
| 16:30 | Tarek Mhamdi, Osman Hasan and Sofiene Tahar On the Formalization of the Lebesgue Integration Theory in HOL |
Monday, July 12th
Monday's program is also available with abstracts and side by side with other events.
09:00‑10:00 ITP Invited Talk
Chair: Sandip Ray
Location: AT LT5
| 09:00 | Gerwin Klein (NICTA) A Formally Verified OS Kernel. Now What? |
10:30‑12:30 Session 4
Chair: J Moore
Location: AT LT5
| 10:30 | Joe Hendrix, Deepak Kapur and Jose Meseguer Coverset Induction with Partiality and Subsorts: a Powerlist Case Study |
| 11:00 | Michaël Armand, Benjamin Grégoire, Arnaud Spiwack and Laurent Théry Extending Coq with Imperative Features and its Application to SAT Verification |
| 11:30 | Moa Johansson, Lucas Dixon and Alan Bundy Case-Analysis for Rippling and Inductive Proof |
| 12:00 | Panagiotis Manolios and Daron Vroon Interactive Termination Proofs using Termination Cores |
14:00‑15:00 Session 5
Chair: Gerwin Klein
Location: AT LT5
| 14:00 | Gilles Barthe, Benjamin Grégoire and Santiago Zanella Béguelin Programming language techniques for cryptographic proofs |
| 14:30 | David Cachera and David Pichardie Proof Pearl: A Certified Denotational Abstract Interpreter |
15:30‑17:00 Session 6
Chair: Pete Manolios
Location: AT LT5
| 15:30 | Sol Swords and Warren Hunt A Mechanically Verified AIG-to-BDD Conversion Algorithm |
| 16:00 | William Mansky and Elsa Gunter A Framework for Formal Verification of Compiler Optimizations |
| 16:30 | Herman Geuvers, Adam Koprowski, Dan Synek and Eelis van der Weegen Automated Machine-Checked Hybrid System Safety Proofs |
Tuesday, July 13th
Tuesday's program is also available with abstracts and side by side with other events.
09:00‑10:00 FLoC Plenary Talk: Georg Gottlob
Chair: Martin Grohe
Location: George Square Lecture Theatre
| 09:00 | Georg Gottlob (University of Oxford) Datalog+-: A Family of Logical Query Languages for New Applications. |
10:30‑12:30 Session 7
Chair: Michael Norrish
Location: AT LT5
| 10:30 | Amy Felty and Brigitte Pientka Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison |
| 11:00 | Serge Autexier and Dominik Dietrich A tactic language for declarative proofs |
| 11:30 | Daria Walukiewicz-Chrząszcz and Jacek Chrząszcz Inductive Consequences in the Calculus of Constructions |
| 12:00 | Magnus O. Myreen Separation logic adapted for proofs by rewriting |
| 12:10 | Douglas Howe Higher-Order Abstract Syntax in Isabelle/HOL |
| 12:20 | Bas Spitters and Eelis van der Weegen Developing the algebraic hierarchy with type classes in Coq |
14:00‑15:00 FLoC Keynote Talk: J Strother Moore
Chair: Jean-Pierre Jouannaud
Location: George Square Lecture Theatre
| 14:00 | J Strother Moore (University of Texas) Theorem Proving for Verification: The Early Days. |
Wednesday, July 14th
Wednesday's program is also available with abstracts and side by side with other events.
09:00‑10:00 ITP Invited Talk
Chair: Christian Urban
Location: AT LT5
| 09:00 | Benjamin C. Pierce (University of Pennsylvania) Proof Assistants as Teaching Assistants: A View from the Trenches |
10:30‑12:30 Session 8
Chair: Thorsten Altenkirch
Location: AT LT5
| 10:30 | Matthieu Sozeau Equations: a dependent pattern-matching compiler |
| 11:00 | Arthur Charguéraud The Optimal Fixed Point Combinator |
| 11:30 | Thomas Braibant and Damien Pous An Efficient Coq Tactic for Deciding Kleene Algebras |
| 12:00 | Peter Lammich and Andreas Lochbihler The Isabelle Collections Framework |
14:00‑15:00 Session 9
Chair: Jose Luis Ruiz-Reina
Location: AT LT5
| 14:00 | Jasmin Christian Blanchette and Tobias Nipkow Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder |
| 14:30 | Alexander Krauss and Andreas Schropp A Mechanized Translation from Higher-Order Logic to Set Theory |
15:30‑17:00 Session 10
Chair: Elsa Gunter
Location: AT LT5
| 15:30 | Chantal Keller and Benjamin Werner Importing HOL-Light into Coq |
| 16:00 | Sascha Böhme and Tjark Weber Fast LCF-Style Proof Reconstruction for Z3 |
| 16:30 | Tjark Weber Validating QBF Invalidity in HOL4 |