[TYPES/announce] Proof Search in Axiomatic Theories and Type Theories (PSATTT'13)

[Stéphane Graham-Lengrand]

                Call for Abstracts & Participation
              PSATTT 2013: International Workshop on
        Proof Search in Axiomatic Theories and Type Theories
                        Palaiseau, France
                        November 8, 2013
     http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT13/

Co-located with the 2013 LIX Colloquium on
The Theory and Application of Formal Proofs.
http://www.lix.polytechnique.fr/colloquium2013/

IMPORTANT DATES
Title and abstract: 15th October
Workshop:            8th November

TALK PROPOSAL
By email to the organisers:
graham-lengrand at lix.polytechnique.fr
assia.mahboubi at inria.fr

DESCRIPTION AND AIMS OF THE WORKSHOP

This workshop continues the series entitled "Proof Search in Type
Theories" (PSTT at CADE'09, FLOC'10) and "Proof Search in Axiomatic
Theories and Type Theories" (PSATTT at CADE'11).

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

Work-in-progress is welcome, as well as system descriptions for new
prototypes or new features implemented in existing tools, with a
demonstration on the day of the workshop.

ORGANISERS
Stéphane Lengrand, CNRS - Ecole Polytechnique, France
Assia Mahboubi, INRIA, France

Contact details:
graham-lengrand at lix.polytechnique.fr
assia.mahboubi at inria.fr