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 Andrew Appel, Dale Miller (moderator), Frank Pfenning, and Benjamin Werner. The slides used by some of the panelist are available: Miller and Werner.

Description: 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.

1. 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 kernels.
2. Can theorem provers output proof evidence that is free from their specific implementation details?
3. 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)?
4. How complex can proof checkers be? Can they contain a programming language? How do we trust a proof checker?
5. 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 for proofs?
6. 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?