Fourth Workshop on Proof eXchange for Theorem Proving

PxTP 2015

Affiliated with the 25th International Conference on Automated Deduction (CADE 25)

August 2-3, 2015, Berlin


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 automated and interactive, during the past decades, 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 also 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 to exchange 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 the interested 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 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:


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. Papers will be submitted via EasyChair, at the PxTP'2015 workshop page. Accepted full papers will appear in an EPTCS volume.

Important dates

Invited speakers


Registration to PxTP is part of the CADE registration process. Delegates registering for either August 2 or August 3 are welcome to all sessions of PxTP.


The PxTP 2015 proceedings are now available. You can also download them as a single PDF file.


Sunday, August 2

9:30-10:30 Invited speaker: Georges Gonthier
Reflection, of all shapes and sizes

10:30-11:00 coffee break
11:00-11:30 Quentin Heath and Dale Miller
A framework for proof certificates in finite state exploration

11:30-12:00 Christoph Benzmüller, Maximilian Claus and Nik Sultana
Systematic Verification of the Modal Logic Cube in Isabelle/HOL

12:00-12:30 Mark Adams
The Common HOL Platform

12:30-14:00 lunch break
14:00-14:30 Giselle Reis
Importing SMT and Connection proofs as expansion trees

14:30-14:50 Mikheil Rukhaia
Theorem Proving in Formula Schemata [presentation only]

14:50-15:30 Discussion session: Encyclopedia of Proof Systems
mediated by Bruno Woltzenlogel Paleo

15:30-16:00 coffee break
16:00-17:00 Panel discussion
moderated by Dale Miller

Monday, August 3

9:30-10:30 Invited speaker: Bart Jacobs
The VeriFast program verifier and its SMT solver interaction

10:30-11:00 coffee break
11:00-11:30 Raphaël Cauderlier and Pierre Halmagrand
Checking Zenon Modulo Proofs in Dedukti

11:30-12:00 Ali Assaf and Guillaume Burel
Translating HOL to Dedukti

12:00-12:30 Ali Assaf and Raphaël Cauderlier
Mixing HOL and Coq in Dedukti

Program committee

Previous editions