[TYPES/announce] CFP: Proof-Search in Type Theories 09

["Stéphane Lengrand (Work)"]

                           Call for Papers
                PSTT 2009: International Workshop on
                    Proof Search in Type Theories

                  McGill University, Montreal, Canada
                             August 3, 2009
       http://www.lix.polytechnique.fr/~lengrand/Events/PSTT09/

Affiliated with CADE-22, Montreal, Canada, August 2-7, 2009
Joint event with the 2009 International Workshop on
Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), 
August 2, 2009

IMPORTANT DATES
Abstract submission: May 1
Paper Submission:    May 8
Notification:        June 15
Final papers due:    July 3
Workshop:            August 3

JOINT LFMTP/PSTT INVITED SPEAKER:
 Gilles Dowek (Ecole Polytechnique & INRIA)
JOINT LFMTP/PSTT TUTORIAL SPEAKER:
 TBA

DESCRIPTION:
The PSTT workshop resumes a series of workshops on Proof Search in
Type Theoretic Languages, in light of the progress that has been made
over the last decade in e.g. the development of proof assistants or
our understanding of proof theory.

The declarative approach to programming has evolved two paradigms that
are based on different aspects of the theories of proofs and types:
Proof normalisation provides a foundation for functional programming
and type systems --on which numerous proof assistants are based, while
proof search provides a foundation for logic programming and other
areas of automated deduction. On the one hand, proof search mechanisms
and their automation are decisive features of proof assitants that
have much to gain from a proper understanding and formalisation. On
the other hand, the framework of logic programming has also extended
to more expressive logics and more complex data structures, e.g. with
bindings.

Better specifying the proof search mechanisms in type theories is thus
a key concern that brings both approaches forward, and closer
together. This concern involves a wide range of issues and techniques
(some of which directly arising from implementation) that both
approaches share --or could share, and that form the scope of this
workshop.

TOPICS:
Papers are solicited on topics including, but not limited to:
- proof search strategies and tactics, complexity & completeness,
- tactics specification language,
- properties of inference systems, invertibility, polarity of connectives,
- focusing, normal forms for proofs,
- proof-term representation,
- meta-variables, representation of partial proofs,
- searching for proofs by induction, search for invariants,
- unification,
- variable binding, scoping management and freshness
- logic programming and other paradigms based on proof search, 
termination & computational expressivity,
- deduction-modulo, deduction vs. computation during search,
- using failure in proof search,
- model checking as deduction,
- user interaction and interfaces,
- systems implementing any of the above.

SUBMISSIONS:
Authors can submit either detailed and technical accounts of new
research or work in progress.  System descriptions are also welcome,
with a demonstration on the day of the workshop. Surveys and
comparative papers are also strongly encouraged.

Papers are to be submitted electronically and are subject to a 12-page
limit in LNCS format, including bibliography. They can be shorter.
Authors are required to submit a paper title and a short abstract one
week before submitting the paper. 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.  The possibility of
having a special issue dedicated to the themes of this workshop is
under consideration.

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

PSTT PROGRAM COMMITTEE:
 Gilles Dowek (Ecole Polytechnique)
 Didier Galmiche (Universite H. Poincare - Nancy 1)
 Stephane Lengrand, Chair (CNRS)
 Brigitte Pientka (McGill University)
 Randy Pollack (University of Edinburgh)