default search action

combined dblp search
author search
venue search
publication search

ask others

PxTP 2012, Manchester, UK

> Home > Conferences and Workshops > PxTP

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/2012
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/2012
David Pichardie, Tjark Weber:
Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012. CEUR Workshop Proceedings 878, CEUR-WS.org 2012

Invited Talks

- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/Constable12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/Constable12
Robert L. Constable:
Proof Assistants and the Dynamic Nature of Formal Theories. 1-15
- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/Merz12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/Merz12
Stephan Merz:
Proofs and Proof Certification in the TLA⁺ Proof System. 16-20

Contributed Papers

- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/StumpRTLEOZ12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/StumpRTLEOZ12
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang:
LFSC for SMT Proofs: Work in Progress. 21-27
- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/BoespflugCH12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/BoespflugCH12
Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant:
The λΠ-calculus Modulo as a Universal Proof Language. 28-43
- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/BoespflugB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/BoespflugB12
Mathieu Boespflug, Guillaume Burel:
CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. 44-50
- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/DunchevLLRRWP12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/DunchevLLRRWP12
Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo:
System Feature Description: Importing Refutations into the GAPT Framework. 51-57
- view
  - electronic edition @ ceur-ws.org
  - details & citations
- export record
  dblp key:
  - conf/pxtp/BessonCS12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pxtp/BessonCS12
Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard:
Walking through the Forest: Fast EUF Proof-Checking Algorithms. 58-64

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.