Dale Miller (INRIA Saclay & LIX/Ecole Polytechnique), Proof certificates as focused sequent proofs



Computational logic systems, such as theorem provers and model checkers, produce evidence of a successful proof in an assortment of (often ad hoc) formats. Unfortunately, the evidence generated by one prover is seldom readable by another prover or even by a future version of itself. As a result, provers seldom trust and use proofs from other provers. This situation is made all the more regrettable given that logic and (formal) proof are certainly candidates for universally accepted standards. I will outline some recent work on designing documents, called proof certificates, that satisfy the following requirements: (i) They are checkable by a simple proof checkers; (ii) They are flexible enough that existing provers can conveniently produce such certificates from their internal evidence of proof; (iii) They are directly related to proofs used within the structural proof theory literature; and (iv) They permit certificates to elide some proof information with the expectation that a proof checker can reconstruct the missing information using bounded and structured proof search. I shall show how the notion of focus sequent proofs can be used to design such proof certificates.