Program

All sessions will take place in Suite 2928 unless otherwise indicated.

Wednesday, August 16th

Wednesday's program is also available with abstracts or side by side with other meetings.

09:15‑09:30  Introductory Remarks

09:30‑10:30  Invited Talk

09:30

Georges Gonthier (Microsoft Research) Internal Deduction and Decision Procedures of the 4-Colour Theorem [ppt]

10:30‑11:00  Break

11:00‑12:30  Session 1

11:00	Adam Chlipala and George Necula Cooperative Integration of an Interactive Proof Assistant and an Automated Prover
11:30	Hongping Lim and Myla Archer Translation Templates to Support Strategy Development in PVS
12:00	Florent Kirchner and Cesar Munoz PVS#: Streamlined Tacticals for PVS

12:30‑14:00  Lunch break

14:00‑15:30  Session 2

14:00	Moa Johansson, Alan Bundy and Lucas Dixon Best-First Rippling
14:30	Maria Paola Bonacina and Mnacho Echenim Rewrite-Based Decision Procedures
15:00	William McCune Semantic Guidance with Carefully Chosen Interpretations

15:30‑16:00  Break

16:00‑17:00  Invited Talk

16:00

José Meseguer (University of Illinois at Urbana-Champaign) Specifying and Implementing Strategies in Rewriting Logic [pdf]

17:00‑17:30  Final Remarks