Workshop Description

The goal of this workshop is to bring together researchers working on proof production from automated theorem provers with potential consumers of proofs. Machine-checkable proofs have been proposed for applications like proof-carrying code and certified compilation, as well as for exchanging knowledge between different automated reasoning systems. For example, interactive theorem provers can import results from otherwise untrusted high-performance solvers, by means of proofs the solvers produce. In such situations, one automated reasoning tool can make use of the results of another, without having to trust that the second tool is sound. It is only necessary to be able to reconstruct a proof that the first tool will accept, in order to import the result without increasing the size of the trusted computing base.

This simple idea of proof exchange for theorem proving becomes quite complicated under the real-world constraints of highly complex and heterogeneous proof producers and proof consumers. For example, even the issue of a standard proof format for a single class of solvers, like SMT solvers, is quite difficult to address, as different solvers use different inference systems. It may be quite challenging, from an engineering and possibly also theoretical point of view, to fit these into a single standard format. Emerging work from several groups proposes standard meta-languages or parametrized formats to achieve flexibility while retaining a universal proof language.

Proceedings

The PxTP 2012 Proceedings have been published at http://ceur-ws.org/Vol-878/ .

Invited Speakers

  • Robert L. Constable, Cornell University, US
  • Stephan Merz, Inria Nancy, France

Program

09:00 - 10:00 Invited Speaker: Robert L. Constable
Proof Assistants and the Dynamic Nature of Formal Theories
Joint speaker with ATX 2012
10:00 - 10:30 coffee break
10:30 - 12:00 Joint session with PAAR-2012
Daniel Kuehlwein and Josef Urban
Learning from Multiple Proofs: First Experiments

Jesse Alama
Escape to Mizar from ATPs

Cezary Kaliszyk and Josef Urban
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
12:00 - 13:30 lunch break
13:30 - 14:30 Invited Speaker: Stephan Merz
Proofs and Proof Certification in the TLA+ Proof System
14:30 - 15:00 Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley D. Eades Iii, Corey Oliver and Ruoyu Zhang
LFSC for SMT Proofs: Work in Progress
15:00 - 15:30 coffee break
15:30 - 17:30 Mathieu Boespflug, Quentin Carbonneaux and Olivier Hermant
The lambda-Pi-calculus Modulo as a Universal Proof Language

Mathieu Boespflug and Guillaume Burel
CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo

Mikheil Rukhaia, Cvetan Dunchev, Alexander Leitsch, Daniel Weller, Tomer Libal, Martin Riener and Bruno Woltzenlogel-Paleo
System Feature Description: Importing Refutations into the GAPT Framework

Ronan Saillard, Frédéric Besson and Pierre-Emmanuel Cornilleau
Walking through the Forest: a Fast EUF Proof-Checking Algorithm

Important Dates

  • Paper submission deadline:
  • April 2nd, 2012  EXTENDED: April 16th, 2012
  • Author notification:
  • May 7th, 2012
  • Camera-ready paper versions due:
  • May 21th, 2012
  • Workshop:
  • June 30th, 2012

    Call For Papers

    [.txt]

    Submission

    Paper should be submitted through the EasyChair page.

    Program Committee

    • Jasmin Blanchette, Technische Universität München, Germany
    • Pascal Fontaine, University of Nancy, France
    • John Harrison, Intel Corporation, USA
    • Leonardo de Moura, Microsoft Research, USA
    • David Pichardie (co-chair), Inria Rennes, France
    • Pierre-Yves Strub, INRIA/Microsoft, France
    • Aaron Stump, The University of Iowa, USA
    • Geoff Sutcliffe, University of Miami, USA
    • Laurent Théry, Inria Sophia-Antipolis, France
    • Allen Van Gelder, University of California at Santa Cruz, USA
    • Tjark Weber (co-chair), Uppsala University, Sweden