[Om-announce] PxTP 2013 - Call for Papers

[Josef Urban]

                       Call for Papers, PxTP 2013

               The Third International Workshop on
            Proof Exchange for Theorem Proving (PxTP)
            (and Cooperation between Theorem Provers)
                   http://www.cs.ru.nl/pxtp13/

                 June 10, 2013, Lake Placid, USA

                         associated with

        The Conference on Automated Deduction (CADE), 2013.

----------------------------------------------------------------------

Invited Speaker

 Thomas C. Hales, University of Pittsburgh

----------------------------------------------------------------------

Scope

The PxTP workshop welcomes contributions on various aspects of
communication, integration, and cooperation between reasoning systems
and formalisms.

The past decades have seen impressive advances in computer-aided
reasoning, both in automated and interactive theorem proving. As shown
by various system competitions, such as CASC, SMT-COMP, and the SAT
competition, deduction tools are able to tackle larger problems
progressively faster and are increasingly more applicable to a wider
range of problems. In recent years, integration of such automated
tools in larger verification environments has demonstrated the
potential to reduce the amount of manual verification work.

It is becoming clear that the success of deduction tools will not only
depend on their power to solve large and difficult problems in an
isolated manner, but it will also rely on their ability to cooperate,
by exchanging problems, proofs, and models. The PxTP workshop aims at
encouraging such cooperation by inviting contributions on various
aspects of communication, integration, and cooperation between systems
and formalisms. The workshop's mission is to facilitate building of
complex reasoning applications and reuse of reasoning tools by
developing and discussing suitable integration, translation and
communication methods, standards, protocols, and application
programming interfaces (APIs).  We are interested both in success
stories and in descriptions of the current bottlenecks and proposals
for improvement.

----------------------------------------------------------------------

Topics of interest for this workshop include all aspects of
cooperation between reasoning tools, whether automatic or interactive.
More specifically, some suggested topics are

-- applications that integrate reasoning tools
   (ideally with certification of the result);

-- translations between logics, proof systems, models;

-- distribution of proof obligations among heterogeneous reasoning
   tools;

-- algorithms and tools for checking and importing (replaying,
   reconstructing) proofs;

-- proposed formats for expressing problems and solutions for
   different classes of logic solvers (SAT, SMT, QBF, first-order
   logic, higher-order logic, typed logic, rewriting, etc.);

-- meta-languages, logical frameworks, communication methods,
   standards, protocols, and APIs connected to problems, proofs, and
   models;

-- comparison, refactoring, and optimization of proofs;

-- practical experiences, case studies, feasibility studies;

-- applications relying on importing proofs from automatic theorem
   provers, such as certified static analysis, proof-carrying code, or
   certified compilation;

-- data structures and algorithms for improved proof production in
   solvers (e.g., efficient proof representations).

----------------------------------------------------------------------

Submissions

Researchers interested in participating are invited to submit either
an extended abstract (up to 8 pages) or a regular paper (up to 15
pages) via EasyChair.

Submissions will be refereed by the program committee, which will
select a balanced program of high-quality contributions.  Short
submissions that could stimulate fruitful discussion at the workshop
are particularly welcome.

Submissions should be in PDF. Final versions should be prepared in
LaTeX using the "easychair.cls" class file, available at
http://www.easychair.org/publications/.

To submit a paper, go to the EasyChair PxTP page
http://www.easychair.org/conferences/?conf=pxtp2013
and follow the instructions there.

PxTP proceedings will be published electronically in the EasyChair
Proceedings in Computing (EPiC) series or in the CEUR workshop
proceedings.

----------------------------------------------------------------------

Important dates

Submission of papers: 11 April 2013
Notification: 2 May 2013
Camera-ready versions due: 9 May 2013
Workshop: 10 June 2013

----------------------------------------------------------------------

Program Committee

Jasmin Christian Blanchette (co-chair), TU Muenchen, Germany
Chad Brown, Saarland University, Germany
David Delahaye, CEDRIC/CNAM, Paris, France
Ewen Denney, SGT/NASA Ames, USA
Peter Dybjer, Chalmers University, Sweden
Pascal Fontaine, Loria, INRIA, University of Nancy, France
Warren Hunt, University of Texas, USA
Chantal Keller, Laboratoire d'Informatique de Polytechnique, France
Konstantin Korovin, Manchester University, UK
Magnus O. Myreen, University of Cambridge, UK
Jens Otten, University of Potsdam, Germany
Andrei Paskevich, Universite Paris-Sud 11, IUT d'Orsay, France
Lawrence C. Paulson, University of Cambridge, UK
David Pichardie, INRIA Rennes - Bretagne Atlantique, France
Florian Rabe, Jacobs University Bremen, Germany
Stephan Schulz, TU Muenchen, Germany
Aaron Stump, CS Department, The University of Iowa, USA
Geoff Sutcliffe, University of Miami, USA
Laurent Thery, INRIA, France
Josef Urban (co-chair), Radboud Universiteit Nijmegen, Netherlands
Tjark Weber, Uppsala University, Sweden

----------------------------------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://openmath.org/pipermail/om-announce/attachments/20130124/5f28db8e/attachment.html>