Foundational proof certificates
Dale Armin Miller · 2013
Consider a world where exporting proof evidence into a declarative, universal, and permanent format is taken as ``feature zero'' for computational logic systems. In such a world, provers will be able to communicate and share theorems and proofs; libraries can archive and organize proofs; and marketplaces of proofs would be open to any prover that admits checkable proof objects. In that world, proof checkers must be entrusted with the task of checking whether or not such proof evidence elaborates into a formal proof. A key to developing such a universal and permanent approach to proof evidence is the selection of an appropriate logical framework for defining the semantics of proof evidence.