PxTP 2012
Proof Exchange for Theorem Proving

Table of Contents

• Front Matter
  
  

Invited Talks

• Proof Assistants and the Dynamic Nature of Formal Theories (invited paper) 1-15
  Robert L. Constable
• Proofs and Proof Certification in the TLA ⁺ Proof System (invited paper) 16-20
  Stephan Merz

Contributed Papers

• LFSC for SMT Proofs: Work in Progress 21-27
  Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades, Corey Oliver, Ruoyu Zhang
• The λΠ-calculus Modulo as a Universal Proof Language 28-43
  Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant
• CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo 44-50
  Mathieu Boespflug, Guillaume Burel
• System Feature Description: Importing Refutations into the GAPT Framework 51-57
  Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel-Paleo
• Walking through the Forest: Fast EUF Proof-Checking Algorithms 58-64
  Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard