Defining the semantics of proof evidence (2015)
(Dale Miller, INRIA Saclay & LIX, FR)

If automatic and interactive theorem provers store completed proofs, they do so using a range of proof structures, such as natural deduction, tableaux, resolution, and winning strategies. Ad hoc prover-specific proof scripts are also commonly used. I will outline how recent results on focused proof systems can be used to provide a formal framework for defining the meaning of a wide range of proof evidence. Interpreters of such formal definitions can thus be used as proof checkers. In order to make it possible to elide many details in formal proofs, proof checkers will be expected to perform significant proof reconstruction via deterministic and non-deterministic computations: such mixing of computation and deduction is an explicit feature of focused proof systems. I will discuss some of the ramifications of employing this framework on the ability of machines and humans to trust and ommunicate formal proofs.

Click for slides.

Due to technical difficulties, the lecture had to be split into three parts and some minutes of the talk may be missing.
​Below is a playlist: