Email Gateway (Aug 22 2022 at 19:29): Email Gateway (Aug 22 2022 at 19:29):From: Mathias Fleury <mathias.fleury12@gmail.com>
[Please accept our apologies for duplicates]
==============================================
Call for Papers, PxTP 2019
The Sixth International Workshop on
Proof eXchange for Theorem Proving (PxTP)
http://pxtp.gforge.inria.fr/2019/ <http://pxtp.gforge.inria.fr/2019/>
25-26 August 2019, Natal, Brazil
associated with the CADE-27 conference
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 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;
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;
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;
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/ <http://style.eptcs.org/>).
Papers will be submitted via EasyChair, at the PxTP'2019 workshop page
(https://easychair.org/conferences/?conf=pxtp2019 <https://easychair.org/conferences/?conf=pxtp2019>).
Accepted regular papers will appear in an EPTCS volume.
TBA
Giselle Reis (Carnegie Mellon University), co-chair
Roberto Blanco, Inria, France
Josef Urban, Czech Institute of Informatics, Robotics and Cybernetics
(CIIRC), Czech Republic
Yoni Zohar, Stanford University, USA
PxTP 2017 (https://pxtp.github.io/2017/ <https://pxtp.github.io/2017/>), affiliated to Tableaux 2017,
FroCoS 2017 and ITP 2017
PxTP 2015 (http://pxtp15.lri.fr/ <http://pxtp15.lri.fr/>), affiliated to CADE-25
Last updated: Apr 19 2024 at 01:05 UTC