A Panel on Communicating and trusting proofs
This panel was held during the
First International Conference on
Certified Programs and Proofs in Kenting, Taiwan on 7 Dec 2011.
The members of this panel were
Frank Pfenning, and
The slides used by some of the panelist are available:
Imagine a world in which computational logic systems (such as theorem
provers, model checkers, type systems, etc) can communicate and trust
proofs on a routine basis. This panel will discuss several issues
concerning such a world. The following questions are suggested to
stimulate the discussion.
- Should we push the de Bruijn criterion (proofs should be checked
by simple kernels) to the next step: require provers to output
proofs into a format that a trusted proof checker can check? In
principle, such a universal checker could replace individual
- Can theorem provers output proof evidence that is free from their
specific implementation details?
- What approaches to communicating and trusting proofs are already
working at some scale: eg, used in SAT competitions, resolution
systems (eg, the Ivy checker), and deduction modulo (Dedukti)?
- How complex can proof checkers be? Can they contain a
programming language? How do we trust a proof checker?
- Is it worthwhile to build the infrastructure of proof
certificates and proof checkers and to modify existing provers to
use that infrastructure? Can we expect such infrastructure to
give rise to new capabilities, such as libraries and marketplaces
- The structure of proofs derive not only from the underlying logic
but also from theories built on top of logics. How are theories
and proofs related? How are two different theories related?