[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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: psatt...@easychair.org