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
09:00‑10:00 Session 1
Chair: Matt Kaufmann [A few short remarks]
09:00 Norbert Schirmer and Ernie Cohen (speaker)
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
09:30 Freek Verbeek (speaker) and Julien Schmaltz
Proof Pearl: A formal proof of Duato's condition for deadlock-free adaptive networks
10:00‑10:30 Coffee break
10:30‑12:30 Session 2
Chair: David Pichardie
10:30 Ramana Kumar (speaker) and Michael Norrish
(Nominal) Unification by Recursive Descent with Triangular Substitutions
11:00 Jean-François Dufourd and Yves Bertot (speaker)
Formal study of plane Delaunay triangulation
11:30 Sylvie Boldo (speaker), 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 (speaker) and Magnus O. Myreen
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
12:30‑14:00 Lunch
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.
15:00‑15:30 Coffee break
15:30‑17:00 Session 3
Chair: Cesar Munoz
15:30 Brian Huffman and Christian Urban (speaker)
Proof Pearl: A New Foundation for Nominal Isabelle
16:00 John Cowles and Ruben Gamboa (speaker)
Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure
16:30 Tarek Mhamdi (speaker), Osman Hasan and Sofiene Tahar
On the Formalization of the Lebesgue Integration Theory in HOL
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
17:00‑18:00 Business Meeting
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