[FOM] Fwd: 6th Workshop on Proof eXchange for Theorem Proving (PxTP) - CFP

Martin Davis martin at eipye.com
Tue Apr 2 12:13:58 EDT 2019

---------- Forwarded message ---------
From: <geoff at cs.miami.edu>
Date: Tue, Apr 2, 2019 at 9:02 AM
Subject: 6th Workshop on Proof eXchange for Theorem Proving (PxTP) - CFP
To: <davism at cs.nyu.edu>

[My apologies if you receive this in duplicate]

Call for Papers, PxTP 2019

        The Sixth International Workshop on
     Proof eXchange for Theorem Proving (PxTP)


           25-26 August 2019, Natal, Brazil

       associated with the CADE-27 conference

## Background

  The PxTP workshop brings together researchers working on various aspects
  communication, integration, and cooperation between reasoning systems and

  The progress in computer-aided reasoning, both automatic and interactive,
  during the past decades, has made it possible to build deduction tools
  are increasingly more applicable to a wider range of problems and are
able to
  tackle larger problems progressively faster. In recent years, cooperation
  such tools in larger verification environments has demonstrated the
  to reduce the amount of manual intervention.  Examples include the
  Sledgehammer tool providing an interface between Isabelle and (untrusted)
  automated provers, and collaboration of the HOL Light and Isabelle
systems in
  the formal proof of the Kepler conjecture.

  Cooperation between reasoning systems relies on availability of
  formalisms and practical tools for exchanging problems, proofs, and
  models. The PxTP workshop strives to encourage such cooperation by
  contributions on suitable integration, translation, and communication
  standards, protocols, and programming interfaces. The workshop welcomes
  developers of automated and interactive theorem proving tools, developers
  combined systems, developers and users of translation tools and
  and producers of standards and protocols.  We are interested both in
  stories and descriptions of current bottlenecks and proposals for

## Topics

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

  * applications that integrate reasoning tools (ideally with certification
    the result);
  * interoperability of reasoning systems;
  * translations between logics, proof systems, models;
  * distribution of proof obligations among heterogeneous reasoning tools;
  * algorithms and tools for checking and importing (replaying,
  * proposed formats for expressing problems and solutions for different
    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 related to problems, proofs, and models;
  * comparison, refactoring, transformation, migration, compression and
    optimization of proofs;
  * data structures and algorithms for improved proof production in
    solvers (e.g., efficient proof representations);
  * (universal) libraries, corpora and benchmarks of proofs and theories;
  * alignment of diverse logics, concepts and theories across systems and
  * engineering aspects of proofs
    (e.g., granularity, flexiformality, persistence over time);
  * proof certificates;
  * proof checking;
  * mining of (mathematical) information from proofs
    (e.g., quantifier instantiations, unsat cores, interpolants, ...);
  * reverse engineering and understanding of formal proofs;
  * universality of proofs
    (i.e. interoperability of proofs between different proof calculi);
  * origins and kinds of proofs
    (e.g., (in)formal, automatically generated, interactive, ...)
  * Hilbert's 24th Problem (i.e. what makes a proof better than another?);
  * social aspects (e.g., community-wide initiatives related to proofs,
    cooperation between communities, the future of (formal) proofs);
  * applications relying on importing proofs from automatic theorem provers,
    such as certified static analysis, proof-carrying code, or certified
  * application-oriented proof theory;
  * practical experiences, case studies, feasibility studies.

## 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).
  Submissions will be refereed by the program committee, which will select a
  balanced program of high-quality contributions. Short submissions that
  stimulate fruitful discussion at the workshop are particularly welcome. We
  expect that one author of every accepted paper will present their work at

  Submitted papers should describe previously unpublished work, and must
  be prepared using the LaTeX EPTCS class (http://style.eptcs.org/).
  Papers will be submitted via EasyChair, at the PxTP'2019 workshop page
  Accepted regular papers will appear in an EPTCS volume.

## Important Dates

  * Abstract submission: May 12, 2019
  * Paper submission: May 19, 2019
  * Notification: June 21, 2019
  * Camera ready versions due: July 14, 2019
  * Workshop: 25-26 August 2019

## Invited Speakers


## Program Committee

  * Haniel Barbosa (University of Iowa), co-chair
  * Giselle Reis (Carnegie Mellon University), co-chair

  * Roberto Blanco, Inria, France
  * Frédéric Blanqui, Inria, France
  * Simon Cruanes, Aesthetic Integration, USA
  * Catherine Dubois, ENSIIE, France
  * Amy Felty, University of Ottawa, Canada
  * Mathias Fleury, Max-Planck-Institut für Informatik, Germany
  * Stéphane Graham-Lengrand, SRI, USA
  * Cezary Kaliszyk, University of Innsbruck, Austria
  * Chantal Keller, LRI, Université Paris-Sud, France
  * Laura Kovács, TU Wien, Austria
  * Olivier Laurent, CNRS, ENS Lyon, France
  * Stefan Mitsch, Carnegie Mellon University, USA
  * Carlos Olarte, UFRN, Brazil
  * Bruno Woltzenlogel Paleo, IOHK, Australia
  * Florian Rabe, LRI, Université Paris-Sud, France
  * Martin Riener, University of Manchester, UK
  * Geoff Sutcliffe, University of Miami, USA
  * Josef Urban, Czech Institute of Informatics, Robotics and Cybernetics
    (CIIRC), Czech Republic
  * Yoni Zohar, Stanford University, USA

## Previous PxTP Editions

  * PxTP 2017 (https://pxtp.github.io/2017/), affiliated to Tableaux 2017,
    FroCoS 2017 and ITP 2017
  * PxTP 2015 (http://pxtp15.lri.fr/), affiliated to CADE-25
  * PxTP 2013 (http://www.cs.ru.nl/pxtp13/), affiliated to CADE-24
  * PxTP 2012 (http://pxtp2012.inria.fr/), affiliated to IJCAR 2012
  * PxTP 2011 (http://pxtp2011.loria.fr/), affiliated to CADE-23
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190402/1a94bafb/attachment.html>

More information about the FOM mailing list