[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
[EMAIL PROTECTED]
Stephane Lengrand
CNRS - Labo d'Info de l'X
