[TYPES/announce] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - DEADLINE EXTENSION: May 5

Fri Apr 23 06:27:13 EDT 2021

             Call for Papers, PxTP 2021

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

            https://pxtp.gitlab.io/2021

                21 July 2021, online

      associated with the CADE-28 conference

## Background

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

   The progress in computer-aided reasoning, both automatic and
   interactive, during the past decades, has made it possible to build
   deduction tools that are increasingly more applicable to a wider range
   of problems and are able to tackle larger problems progressively
   faster. In recent years, cooperation of such tools in larger
   verification environments has demonstrated the potential 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
   theoretical formalisms and practical tools for exchanging problems,
   proofs, and models. The PxTP workshop strives to encourage such
   cooperation by inviting contributions on suitable integration,
   translation, and communication methods, standards, protocols, and
   programming interfaces. The workshop welcomes developers of automated
   and interactive theorem proving tools, developers of combined systems,
   developers and users of translation tools and interfaces, and
   producers of standards and protocols. We are interested both in
   success stories and descriptions of current bottlenecks and proposals
   for improvement.

## Topics

   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);
   * 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,
     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 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 libraries;
   * 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 compilation;
   * 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 could stimulate fruitful discussion at the workshop
   are particularly welcome. We expect that one author of every accepted
   paper will present their work at the workshop.

   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'2021 workshop page
   (https://easychair.org/conferences/?conf=pxtp-7).
   Accepted regular papers will appear in an EPTCS volume.

## Important Dates

   * Abstract submission: *April 28*, 2021
   * Paper submission: *May 5*, 2021
   * Notification: May 26, 2021
   * Camera ready versions due: June 16, 2021
   * Workshop: July 11, 2021 (online)

## Invited Speakers

   TBA

## Program Committee

   * Haniel Barbosa (Universidade Federal de Minas Gerais (UFMG), Belo
     Horizonte, Brazil)
   * Denis Cousineau (Mitsubishi, France)
   * Stefania Dumbrava (ENSIIE, France)
   * Katalin Fazekas (TU Wien, Austria)
   * Mathias Fleury (Johannes Kepler University Linz, Austria), co-chair
   * Predrag Janičić (University of Belgrade, Serbia)
   * Chantal Keller (LRI, Université Paris-Saclay, France), co-chair
   * Aina Niemetz (Stanford University, USA)
   * Jens Otten (University of Oslo, Norway)
   * Giselle Reis (CMU-Qatar, Qatar)
   * Geoff Sutcliffe (University of Miami, USA)
   * François Thiré (Nomadic Labs, France)
   * Sophie Tourret (Max-Planck-Institut für Informatik, Germany)
   * Josef Urban (Czech Institute of Informatics, Czech Republic)

## Previous PxTP Editions

   * PxTP 2019 (http://pxtp.gforge.inria.fr/2019), affiliated to CADE-27
   * 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