Program of ITP (with links to slides and business meeting agenda and minutes)

Note: Follow this link to access the proceedings, Springer LNCS 6172.

This page was derived from the original ITP 2010 program page maintained for ITP 2010 by FLOC 2010.


Sunday, July 11th

14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
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.

Monday, July 12th

Chair: Sandip Ray
09:00 Gerwin Klein (NICTA)
A Formally Verified OS Kernel. Now What? [PDF] [Keynote]
10:00‑10:30 Coffee break
10:30‑12:30 Session 4
Chair: J Moore
10:30 Joe Hendrix (speaker), 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 (speaker)
Extending Coq with Imperative Features and its Application to SAT Verification
11:30 Moa Johansson (speaker), Lucas Dixon and Alan Bundy
Case-Analysis for Rippling and Inductive Proof
12:00 Panagiotis Manolios (speaker) and Daron Vroon
Interactive Termination Proofs using Termination Cores
12:30‑14:00 Lunch
14:00‑15:00 Session 5
Chair: Gerwin Klein
14:00 Gilles Barthe, Benjamin Grégoire and Santiago Zanella Béguelin (speaker)
Programming language techniques for cryptographic proofs
14:30 David Cachera and David Pichardie (speaker)
Proof Pearl: A Certified Denotational Abstract Interpreter
15:00‑15:30 Coffee break
15:30‑17:00 Session 6
Chair: Pete Manolios
15:30 Sol Swords and Warren Hunt
A Mechanically Verified AIG-to-BDD Conversion Algorithm
16:00 William Mansky (speaker) and Elsa Gunter
A Framework for Formal Verification of Compiler Optimizations
16:30 Herman Geuvers, Adam Koprowski, Dan Synek and Eelis van der Weegen (speaker)
Automated Machine-Checked Hybrid System Safety Proofs
Chair: Matt Kaufmann and Michael Norrish

Tuesday, July 13th

Chair: Martin Grohe
09:00 Georg Gottlob (University of Oxford)
Datalog+-: A Family of Logical Query Languages for New Applications.
10:00‑10:30 Coffee break
10:30‑12:30 Session 7
Chair: Michael Norrish
10:30 Amy Felty (speaker) and Brigitte Pientka
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
11:00 Serge Autexier and Dominik Dietrich (speaker)
A tactic language for declarative proofs
11:30 Daria Walukiewicz-ChrzÄ…szcz and Jacek ChrzÄ…szcz (speaker)
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 (speaker) and Eelis van der Weegen
Developing the algebraic hierarchy with type classes in Coq
12:30‑14:00 Lunch
14:00‑15:00 FLoC Keynote Talk: J Strother Moore
Chair: Jean-Pierre Jouannaud
14:00 J Strother Moore (University of Texas)
Theorem Proving for Verification: The Early Days.
15:00‑15:30 Coffee break
15:30‑18:00 Excursion [Information] [sign-up]
19:00‑23:00 FLoC Banquet at Our Dynamic Earth
One of Edinburgh's most popular tourist attractions, by the foot of the Royal Mile. The displays will be open for viewing.

Wednesday, July 14th

Chair: Christian Urban
09:00 Benjamin C. Pierce (University of Pennsylvania)
Proof Assistants as Teaching Assistants: A View from the Trenches
10:00‑10:30 Coffee break
10:30‑12:30 Session 8
Chair: Thorsten Altenkirch
10:30 Matthieu Sozeau
Equations: a dependent pattern-matching compiler
11:00 Arthur Charguéraud
The Optimal Fixed Point Combinator
11:30 Thomas Braibant (speaker) and Damien Pous
An Efficient Coq Tactic for Deciding Kleene Algebras
12:00 Peter Lammich and Andreas Lochbihler
The Isabelle Collections Framework
12:30‑14:00 Lunch
14:00‑15:00 Session 9
Chair: Jose Luis Ruiz-Reina
14:00 Jasmin Christian Blanchette (speaker) and Tobias Nipkow
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
14:30 Alexander Krauss (speaker) and Andreas Schropp
A Mechanized Translation from Higher-Order Logic to Set Theory
15:00‑15:30 Coffee break
15:30‑17:00 Session 10
Chair: Elsa Gunter
15:30 Chantal Keller (speaker) and Benjamin Werner
Importing HOL-Light into Coq
16:00 Sascha Böhme (speaker) and Tjark Weber
Fast LCF-Style Proof Reconstruction for Z3
16:30 Tjark Weber
Validating QBF Invalidity in HOL4