|When?||Thursday 5th June and Friday 6th June 2008|
|Where?||LIX, Ecole Polytechnique, Palaiseau (Paris area), France|
Main seminar room
Places to stay, on Catuscia Palamidessi's webpage
|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
-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.