Program of ITP

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
17:00‑18:00 Business Meeting
Chair: Matt Kaufmann and Michael Norrish
Location: AT LT5
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