*** Deadline extended to April 16th, 2012 ***

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

               The Second International Workshop on
            Proof Exchange for Theorem Proving (PxTP)
                     http://pxtp2012.inria.fr

                         associated with 

       The International Joint Conference on Automated Reasoning
                          (IJCAR), 2012

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

The goal of this workshop is to bring together researchers working
on proof production from automated theorem provers with potential
consumers of proofs.  Machine-checkable proofs have been proposed for
applications like proof-carrying code and certified compilation, as
well as for exchanging knowledge between different automated reasoning
systems.  For example, interactive theorem provers can import results
from otherwise untrusted high-performance solvers, by means of proofs
the solvers produce.  In such situations, one automated reasoning tool
can make use of the results of another, without having to trust that
the second tool is sound.  It is only necessary to be able to
reconstruct a proof that the first tool will accept, in order to
import the result without increasing the size of the trusted computing
base.

This simple idea of proof exchange for theorem proving becomes quite
complicated under the real-world constraints of highly complex and
heterogeneous proof producers and proof consumers.  For example, even
the issue of a standard proof format for a single class of solvers,
like SMT solvers, is quite difficult to address, as different solvers
use different inference systems.  It may be quite challenging, from an
engineering and possibly also theoretical point of view, to fit these
into a single standard format.  Emerging work from several groups
proposes standard meta-languages or parametrized formats to achieve
flexibility while retaining a universal proof language.

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

Topics of interest for this workshop include all aspects of proof
exchange among automated reasoning tools.  More specifically, some
suggested topics are:

-- proposed proof formats for different classes of logic solvers (SAT,
   SMT, QBF, First-Order ATP, Higher-Order ATP, Rewriting, etc.).

-- meta-languages and logical frameworks for proofs, particularly 
   proof systems designed for solvers.

-- proof checking tools and algorithms.

-- proof translation and methods for importing proofs, including proof
   replaying or reconstruction.

-- tools and case studies related to analyzing proofs produced by
   solvers, and proof metrics.

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

-- data structures and algorithms for improved proof production in
   solvers (for example, more time- or memory-efficient ways of
   representing proofs).

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

Invited Speakers 

* Stephan Merz, Inria Nancy, France
* Second Speaker: TBC

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

Submissions

Submitted papers must fall into one of the following two categories:

* Short papers: up to 6 pages, work in progress, experience reports, 
  tool presentations or position statements
* Regular papers: 12-15 pages, research papers

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 standard-conforming Postscript or PDF.  Final
versions should be prepared in LaTeX using the easychair.cls class
file.

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

PxTP will have no formal proceedings, but we intend to provide
electronic proceedings on the CEUR-WS website.

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

Important dates

Submission of papers: April 16th, 2012 (* extended *)
Notification: May 7th, 2012
Camera-ready versions due: May 21th, 2012 
Workshop: June 30th, 2012

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

Program Committee

Jasmin Blanchette, Technische Universität München, Germany
Pascal Fontaine, University of Nancy, France
John Harrison, Intel Corporation, USA
Leonardo de Moura, Microsoft Research, USA
David Pichardie (co-chair), INRIA Rennes, France
Pierre-Yves Strub, INRIA/Microsoft, France
Aaron Stump, The University of Iowa, USA
Geoff Sutcliffe, University of Miami, USA
Laurent Théry, INRIA Sophia-Antipolis, France
Allen Van Gelder, University of California at Santa Cruz, USA
Tjark Weber (co-chair), Uppsala University, Sweden

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