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.
The PxTP 2012 Proceedings have been published at http://ceur-ws.org/Vol-878/ .
- Robert L. Constable, Cornell University, US
- Stephan Merz, Inria Nancy, France
|09:00 - 10:00||Invited Speaker: Robert L. Constable
Proof Assistants and the Dynamic Nature of Formal Theories
This lecture will consider lessons from a decade long effort to explore and advance the logic of events using the Nuprl proof assistant operating in its logical programming environment. It will examine the impact of extensions to the underlying constructive type theory and the programming environment over this period, one of which led to the solution of a long standing open problem in constructive logic. I will also illustrate methods of proof exchange between versions of this theory that are based on replaying results as the theory is extended. This method seems promising for proof exchange among proof assistants based on the LCF tactic mechanism as the main method for building proofs.Joint speaker with ATX 2012
Both theory exploration and proof exchange illustrate the dynamic nature of formal theories created using modern proof assistants and dispel the false impression that formal theories are rigid and brittle objects that become less relevant over time in a fast moving field like computer science.
The ideas I am discussing here are based on the work of the Cornell PRL research group, in particular our research on the logic of events by Mark Bickford, Richard Eaton, and Vincent Rahli, and by our collaboration with David Guaspari of ATC-NY corporation.
|10:00 - 10:30||coffee break|
|10:30 - 12:00||Joint session with
Daniel Kuehlwein and Josef Urban
Learning from Multiple Proofs: First Experiments
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
TLA+ is a specification language originally designed for specifying concurrent and distributed systems and their properties. It is based on Zermelo-Fraenkel set theory for modeling data structures and on the linear-time temporal logic TLA for specifying system executions and their properties. The TLA+ proof system (TLAPS) has been designed as an interactive proof assistant for deductively verifying TLA+ specifications. Designed to be independent of any particular theorem prover, it is based on a hierarchical proof language. A proof manager interprets this language and generates proof obligations corresponding to leaf proofs, which can be discharged by different back-end provers. The current release, restricted to non-temporal reasoning, includes Isabelle/TLA+, an encoding of the set theory underlying TLA+ as an object logic in the proof assistant Isabelle, the tableau prover Zenon, and a back-end for SMT solvers.
This talk will first give an overview of the overall design of TLAPS and its proof language and then focus on proof certification in TLAPS. Since the use of different back-end provers raises legitimate concerns about the soundness of the integration, we expect back-end provers to produce proofs that can be checked by Isabelle/TLA+, our most trusted back-end, and this is currently implemented for the Zenon back-end. I will review our experiences with proof certification, and to what extent it has contributed to avoiding soundness bugs, and will indicate future work that we intend to carry out in order to improve our confidence in the soundness of TLAPS.
|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
|April 2nd, 2012 EXTENDED: April 16th, 2012|
|May 7th, 2012|
|May 21th, 2012|
|June 30th, 2012|
Call For Papers[.txt]
SubmissionPaper should be submitted through the EasyChair page.
- 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