From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id ADAA37F6CB for ; Tue, 10 Feb 2015 10:45:09 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of andrei@tertium.org) identity=pra; client-ip=209.85.215.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="andrei@tertium.org"; x-sender="andrei@tertium.org"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of andrei@tertium.org) identity=mailfrom; client-ip=209.85.215.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="andrei@tertium.org"; x-sender="andrei@tertium.org"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-la0-f42.google.com) identity=helo; client-ip=209.85.215.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="andrei@tertium.org"; x-sender="postmaster@mail-la0-f42.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AFBADM0dlUlCrXVdFcg1hegn6wZAGPIgqHCwdDAQEBAQEBEAEBAQEHCwsJEjCEJQsGQgMiFQUKAiYCJBIBBQE+EgeICw2nK4MrPjGLLpcpCoEXiyaFZAwvEYExBYRQjiGCEYNMgU6PXhIjgRWBZwEKAQEBPIFgPYJzAQEB X-IPAS-Result: A0AFBADM0dlUlCrXVdFcg1hegn6wZAGPIgqHCwdDAQEBAQEBEAEBAQEHCwsJEjCEJQsGQgMiFQUKAiYCJBIBBQE+EgeICw2nK4MrPjGLLpcpCoEXiyaFZAwvEYExBYRQjiGCEYNMgU6PXhIjgRWBZwEKAQEBPIFgPYJzAQEB X-IronPort-AV: E=Sophos;i="5.09,549,1418079600"; d="scan'208";a="121070684" Received: from mail-la0-f42.google.com ([209.85.215.42]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Feb 2015 10:45:09 +0100 Received: by labhz20 with SMTP id hz20so18970086lab.0 for ; Tue, 10 Feb 2015 01:45:08 -0800 (PST) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:sender:from:date:message-id:subject :to:content-type:content-transfer-encoding; bh=xGiWUMLGP+GC4YI/DbLKjKcNDmH8hrcRduqAQUJzvQU=; b=WugK6MS5n5+xonRjlgvWKjlIfL/EzzTenV0IXq85ukXLTeYgtHiDx1C8VLZetiotk9 ob8jQxG/SwC5Y/2H0VE4Z02juFhAhsg7LIO63gHLGExlFQ/B4UGvNxtH/wkSxYrVtoRK dvmBtAyXkwxq36Li5ZyyajYsjezgkqOQ8fVjkQ5WvOn4oKg0v9Mi7CjZmQzR9Ujhe9Ng 2dU/UAZC6IxKIqJu+FNWc8BBO8pbmoSVhTJoesb0Q5YKCp+1NChIzod6eubUFXEtpCSB m1Bc94BcCzcdfx/0vW88C9+SbStmPNiZtzQohloSBYbefzTLvkZZZ52NE8FJxCskjxof j9rQ== X-Gm-Message-State: ALoCoQkgLgg+DK9qMQJx3GyigE79fKqA2FNxbpP2gxJWFDK4b9LHpB+P6/yLcBM1G8jjI6TUmgnA X-Received: by 10.152.2.227 with SMTP id 3mr2599293lax.85.1423561508182; Tue, 10 Feb 2015 01:45:08 -0800 (PST) MIME-Version: 1.0 Sender: andrei@tertium.org Received: by 10.112.218.9 with HTTP; Tue, 10 Feb 2015 01:44:47 -0800 (PST) From: Andrei Paskevich Date: Tue, 10 Feb 2015 10:44:47 +0100 X-Google-Sender-Auth: DNGz5cP93xFnTnUVZ8BuIUJy5Qg Message-ID: To: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Validation-by: andrei@tertium.org Subject: [Caml-list] First Call for Papers, PxTP 2015 The Fourth International Workshop on Proof eXchange for Theorem Proving (PxTP) http://pxtp15.lri.fr/ August 2-3, 2015, Berlin, Germany associated with CADE 2015 Important dates * Abstract submission: Thu, May 7, 2015 * Paper submission: Thu, May 14, 2015 * Notification: Tue, June 16, 2015 * Camera ready versions due: Thu, June 25, 2015 * Workshop: August 2-3, 2015 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); * 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 connected to problems, proofs, and models; * comparison, refactoring, and optimization of proofs; * practical experiences, case studies, feasibility studies; * applications relying on importing proofs from automatic theorem provers, such as certified static analysis, proof-carrying code, or certified compilation; * data structures and algorithms for improved proof production in solvers (e.g., efficient proof representations). 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'2015 workshop page (http://www.easychair.org/conferences/?conf=3Dpxtp2015). Accepted full papers will appear in an EPTCS volume. Invited speakers (joint with the AMI'2015 workshop) * Georges Gonthier (Microsoft Research) * Bart Jacobs (KU Leuven) Program committee * Jesse Alama (Vienna University of Technology) * Peter Baumgartner (NICTA) * Jasmin Blanchette (TU M=C3=BCnchen) * Guillaume Burel (C=C3=89DRIC, ENSIIE) * =C3=89velyne Contejean (LRI, CNRS, Universit=C3=A9 Paris Sud) * Cezary Kaliszyk (University of Innsbruck), co-chair * Ramana Kumar (University of Cambridge) * Dale Miller (Inria / LIX, =C3=89cole polytechnique) * Bruno Woltzenlogel Paleo (Vienna University of Technology) * Andrei Paskevich (LRI, Universit=C3=A9 Paris Sud), co-chair * Damien Pous (LIP, CNRS, ENS Lyon) * Geoff Sutcliffe (University of Miami) * Laurent Th=C3=A9ry (Inria) * Cesare Tinelli (University of Iowa) * Josef Urban (Radboud University Nijmegen)