[TYPES/announce] CfP: Proof-Search in Axiomatic Theories and Type Theories 2011

[Stephane Lengrand (Work)]

                         Call for Papers
              PSATTT 2011: International Workshop on
        Proof Search in Axiomatic Theories and Type Theories
                        Wroclaw, Poland
                        August 1, 2011
     http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT11/

Affiliated with CADE, Wroclaw, Poland
Joint invited talk with the PxTP workshop.

IMPORTANT DATES
Paper / long abstract submission:  May 2
Notification:                      May 30
Final papers due:                  June 27
Workshop:                          August 1

DESCRIPTION AND AIMS OF THE WORKSHOP

This workshop continues the series entitled "Proof Search in Type
Theories" (PSTT at CADE'09, FLOC'10), and enlarges its scope to
encompass proof search in axiomatic theories as well.

Generic proof-search in propositional and first-order logic (even
second-order, higher-order) are fields that already benefit from a
long research experience, spanning from techniques as old as
unification to more recent concepts such as focusing and polarisation.

More adventurous is the adaptation of generic proof-search mechanisms
to the specificities of particular theories, whether these are
expressed in the form of axioms or expressed by sophisticated typing
systems or inference systems.

The aim of this workshop is to discuss proof search techniques when
these are constrained or guided by the shape of either axioms or
inference/typing rules.  But it more generally offers a natural (and
rather informal) venue for discussing and comparing techniques arising
from communities ranging from logic programming to type theory-based
proof assistants, or techniques imported from the fields of automated
reasoning and SMT but with an ultimate view to build proofs or at
least provide proof traces.

============================
Topics of the workshop include, but are not limited to:

- invertibility of deductive rules, polarity of connectives and focusing
devices,
- more generally, development and application of theorems establishing
the existence of normal forms for proofs,
- explicit proof-term representations and dynamic proof-term
construction during proof-search,
- use of meta-variables to represent unknown proofs to be found,
- use of failure and backtracking in proof search,
- integration of rewriting or computation into deductive systems, as
organised by e.g. deduction-modulo
- integration of domain-specific algorithms into generic deductive systems
- transformation of goals into particular shapes that can be treated by
domain-specific tactics or external tools
- externalisation of some proof searching tasks and interpretation of
the obtained outputs (justifications, execution traces...)
- more generally, interfaces between cooperating tools
- importation of automated reasoning techniques and SMT techniques to
proof-constructing frameworks
- quantifier instantiation in SMT techniques, arbitrary alternation of
forall/exists quantifiers
- unification in particular theories or in sophisticated typing systems

More generally, contributions about the following topics are welcome
- proof search strategies, their complexity and the trade-off between
completeness and efficiency,
- searching for proofs by induction, finding well-founded induction
measures, strengthening goals to be
proved by induction, etc,
- reasoning on syntaxes with variable binding (in e.g. quantifiers or
data structures),
- termination, computational expressivity of related programming paradigms,
- user interaction and interfaces,
- systems implementing any of the ideas described above.

Synthesising some of the above aspects into unifying theories is a
concern of our research theme that aims at bringing together research
efforts of different communities, enhancing their
interaction. Contributions made in a spirit of synthesis are thus
particularly welcome.
==============================
SUBMISSIONS:

Authors can submit either detailed and technical accounts of new
research or work in progress. Surveys and comparative papers are also
strongly encouraged.

Papers / long abstracts are to be submitted electronically and are
subject to a 15-page limit in LNCS format, including
bibliography. They can be shorter.
System description are also welcome, with an 8-page limit and a
demonstration on the day of the workshop.

At least one author of an accepted paper is expected to present that
paper at the workshop.  Informal proceedings will be distributed at
the workshop. PSATTT and PxTP are in the process of organizing a
special issue in a journal, dedicated to their themes. The call will
be open to everyone but will concern in particular the research
material presented at PSATTT'11 and PxTP'11, as well as PSTT'08,
PSTT'09 and PSTT'10. A specific refereeing round will ensure journal
quality of the selected papers.

For further information and submission instructions, see the PSTT web
page: http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT11/

PROGRAM COMMITTEE:
Jeremy Avigad,     Carnegie Mellon University
Evelyne Contejean, CNRS - INRIA Saclay
Amy Felty,         University of Ottawa
Stephane Lengrand, CNRS - Ecole Polytechnique
David Pichardie,   INRIA Rennes
Aaron Stump,       University of Iowa
Enrico Tassi,      INRIA Microsoft Research joint centre

ORGANISERS
Germain Faure, INRIA, France
Stephane Lengrand, CNRS, France
Assia Mahboubi, INRIA, France

Contact details:
psattt11 at easychair.org