Programme

Thursday 5th June and Friday 6th June 2008
LIX, Ecole Polytechnique

Slots are deliberately long to allow for discussions and mid-talk questions. Talks can be short, we can just use the extra time for an extra break.

Thursday 5th June

10:00 : Free distribution of coffee and hopefully croissants

10:30 : Dale Miller, Higher-order unification as proof-search

11:15 : Daniel Méry, Relation-based Calculi for Propositional Intuitionistic Logic

12:00 : Fredrik Lindblad, Automated proof construction based on first-order narrowing

12:45 : LUNCH (check out meal tickets)

14:15 : Sabine Broda, Formula-Tree Proof method

15:00 : Lutz Strassburger, Things are different with deep inference

15:45 : Pause

16:15 : Stephane Lengrand, Sequent Calculus: An adequate formalism for proof search & unification

16:45 : Small business meeting

Afterwards : Going for dinner in town? Here are suggestions in the neighbourhood
(email me if you think you will come, so I have a idea of numbers)

Friday 6th June

9:30 : Coffee and co.

10:15 : Gilles Dowek, Reducing nominal unification to pattern unification (joint ongoing work with Jamie Gabbay)

11:00 : Short Pause

11:15 : Arnaud Spiwack, Coq's Proof Search (somewhat) Unleashed

12:00 : Sean McLaughlin, The focused inverse method for intuitionistic propositional and first-order logic

12:45 : LUNCH (check out meal tickets)

14:00 : Guillaume Burel, Using focusing to search for proofs in pure type systems

14:45 : Clement Houtmann, Axiom directed focusing