Friday 9 February 2016, 11:00: Quis custodiet ipsos custodes? - Trusting theorem provers, Giselle Reis (Inria).

As theorem provers become increasingly efficient, their code-bases become more complicated, using sophisticated algorithms and optimizations that are rarely considered on the theoretical counter-part. Sometimes, for the sake of efficiency, one needs even to give up completeness. Coupled with this is the fact that different theorem provers implement different calculi and, thus, produce different proof objects that cannot be understood but by a dedicated parser/interpreter.

In such scenario, we ask ourselves how to trust theorem provers. It is an overwhelming task and so far people have concentrated in developing a syntax for proof objects of a certain kind (SAT, resolution, SMT), building bridges between pairs of theorem provers by translating the output of one into another (checking HOL proofs in Coq), or using other theorem provers to check parts of a proof (DVDV checker for TPTP). The proofcert project aims for a more general and fundamental approach: define a framework for specifying semantics of all proof objects.

In this talk I will talk about this big effort, explain the framework chosen and how it is used to check proofs. I will also present the results of our effort to check proofs from Eprover and the challenges we need to overcome next.