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, USA ---------------------------------------------------------------------- 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 (updated) Submission of papers: 22 April 2013 Notification: 9 May 2013 Camera-ready versions due: 16 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 John Harrison, Intel Corporation, USA 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 ----------------------------------------------------------------------