[ 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

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
-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

Stephane Lengrand
CNRS - Labo d'Info de l'X

Reply via email to