[TYPES/announce] "Proof-search in Type Theories" workshop, 5th June, Paris: Call for talks / participation

["Stéphane Lengrand (Work)"]

Please feel free to forward this announcement to people who could be 
interested.
 
Call for talks / participation

Workshop on
*"Proof-search in Type Theories"*

*Thursday 5th June*
(+ possibly Friday 6th June if we have more talks than what fits in a day)

Laboratoire d'Informatique de l'Ecole Polytechnique,
Palaiseau, France

Details can be found (and will be updated) at
http://www.lix.polytechnique.fr/~lengrand/Workshop/

================================
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. Issues that are clearly in the scope include 
for instance:
-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.
================================

If you are interested in participating to the workshop, and possibly 
offer a talk, please email
Lengrand at lix.polytechnique.fr

Stephane Lengrand
CNRS - Labo d'Info de l'X
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20080507/b979f526/attachment.htm