=Paper=
{{Paper
|id=None
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-878/frontmatter.pdf
|volume=Vol-878
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-878/frontmatter.pdf</pdf>
<pre>
Proof Exchange for Theorem Proving —
   Second International Workshop,
             PxTP 2012




             Manchester, UK
              June 30, 2012




                 Proceedings




      Edited by David Pichardie and Tjark Weber
Copyright c 2012 for the individual papers by the papers’ authors. Copying permitted for
private and academic purposes. This volume is published and copyrighted by its editors.
Preface
The goal of the PxTP workshop series is to bring together researchers working on proof produc-
tion 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 exam-
ple, 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 parametrised formats to achieve flexibility while retaining a universal proof
language.
     PxTP 2012, the Second International Workshop on Proof Exchange for Theorem Proving,
was held as a satellite event of IJCAR on June 30, 2012, in Manchester, UK. The workshop
featured invited talks by Robert L. Constable and Stephan Merz, a joint session with the Third
Workshop on Practical Aspects of Automated Reasoning (PAAR 2012), and presentations of
the five accepted papers that are collected in this volume. We would like to thank the IJCAR
organisers, the PxTP program committee, the authors and speakers, and everyone else who
contributed to the workshop’s success.

David Pichardie and Tjark Weber
Co-chairs, PxTP 2012




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, 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, Uppsala University, Sweden
Contents


Invited Talks
Proof Assistants and the Dynamic Nature of Formal Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
  Robert L. Constable

Proofs and Proof Certification in the TLA+ Proof System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
  Stephan Merz


Contributed Papers
LFSC for SMT Proofs: Work in Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
  Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades,
  Corey Oliver, and Ruoyu Zhang

The λΠ-calculus Modulo as a Universal Proof Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant

CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo 44
  Mathieu Boespflug and Guillaume Burel

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

Walking through the Forest: Fast EUF Proof-Checking Algorithms . . . . . . . . . . . . . . . . . . . . . . . 58
  Frédéric Besson, Pierre-Emmanuel Cornilleau, and Ronan Saillard

</pre>