Workshop on "Proof-search in Type Theories"

When? Thursday 5th June and Friday 6th June 2008
Where? LIX, Ecole Polytechnique, Palaiseau (Paris area), France
Main seminar room
Access
Places to stay, on Catuscia Palamidessi's webpage
What? Programme
Who? List of participants (to be confirmed/updated)
Where shall we have dinner? Suggestions in the neighbourhood

Following discussions between the Parsifal and TypiCal teams at Polytechnique, we organise an event on the topic of the search for proofs -or type inhabitants / functional programs- in various logics / type theories.
The aim is to share the insights of communities whose research revolves around pure Logic Programming or the Curry-Howard correspondence, Type Theory, and the proof-assistants based on them.
Welcome topics range from proof-search tactics in proof-assistants, their interface and their automation, to the notion of proof-search as a computational paradigm, with various degrees of user interaction in-between. Any logic (intuitionistic, classical, linear, etc...) and any formalism (sequent calculus, natural deduction, deep inference, graphs, etc...) is welcome. Related issues are for example:
-incomplete proofs and the use of meta-variables
-focused sequent calculi
-unification
-induction (search for proofs by...)
-binders in object-syntax
...
A small "business meeting" will be scheduled as to discuss the motivation for exchanges on the theme, and potential future collaborations, partnerships, implementation projects, applications for grants, a regular workgroup, or a workshop affiliated to a conference... thereon.