[TYPES/announce] PxTP: Third Call for Papers (New Deadline: 26th of June)

Wed Jun 14 02:05:56 EDT 2017

            Call for Papers, PxTP 2017  

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

          https://pxtp.github.io/2017/  

     23-24 September 2017, Brasilia, Brazil  

                associated with  

     The Tableaux, FroCoS and ITP conferences  

## 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 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  

 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;  

 * 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'2017 workshop page  
 (https://easychair.org/my/conference.cgi?a=12750890;welcome=1;conf=pxtp2017).  
 Accepted regular papers will appear in an EPTCS volume.  

## Important Dates  

 * Abstract submission: Monday, 26 June 2017  
 * Paper submission: Monday, 26 June 2017  
 * Notification: Friday, 7 July 2017  
 * Camera ready versions due: Friday, 21 July 2017  
 * Workshop: 23-24 September 2017  

## Invited Speakers  

 * Gilles Dowek (INRIA)  
 * Cesare Tinelli (The University of Iowa)  

## Program Committee  

 * Catherine Dubois (ENSIIE-Samovar), co-chair  
 * Bruno Woltzenlogel Paleo, co-chair  

 * Christoph Benzmüller (Freie Universität Berlin)  
 * Jasmin Christian Blanchette (INRIA Nancy & LORIA)  
 * Hans De Nivelle (Institute of Computer Science, University of Wroclaw)  
 * Pascal Fontaine (Loria, INRIA, University of Lorraine)  
 * Stéphane Graham-Lengrand (CNRS - INRIA - Ecole Polytechnique)  
 * Hugo Herbelin (INRIA)  
 * Olivier Hermant (MINES ParisTech)  
 * Cezary Kaliszyk (University of Innsbruck)  
 * Guy Katz (Stanford University)  
 * Chantal Keller (LRI, Université Paris-Sud)  
 * Tomer Libal (INRIA)  
 * Mariano Moscato (National Institute of Aerospace)  
 * Vivek Nigam (Universidade Federal da Paraíba)  
 * Andrei Paskevich (Université Paris-Sud, LRI)  
 * Florian Rabe (Jacobs University Bremen)  
 * Andrew Reynolds (University of Iowa)  
 * Stephan Schulz (DHBW Stuttgart)  
 * Geoff Sutcliffe (University of Miami)  
 * Josef Urban (Czech Technical University in Prague)  
 * Tjark Weber (Uppsala University)  
 * Akihisa Yamada (University of Innsbruck)    

## Previous PxTP Editions  

 * PxTP 2011 (http://pxtp2011.loria.fr/), affiliated to CADE-23  
 * PxTP 2012 (http://pxtp2012.inria.fr/), affiliated to IJCAR 2012  
 * PxTP 2013 (http://www.cs.ru.nl/pxtp13/), affiliated to CADE-24  
 * PxTP 2015 (http://pxtp15.lri.fr/), affiliated to CADE-25  
![](https://link.nylas.com/open/3x691kf2sejzsuk0agjgff6ov/local-27e52018-19ad)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20170614/993a95b9/attachment-0001.html>