[Show/Hide Left Column]

Place: LRI, building 650, room 455

13h45 - 14h : welcome

14h - 14h45 : Guillaume Bury (LSV)
Title: Proving your proof
Theorem provers have now become very big pieces of code, implementing complex algorithm in an efficient manner, and relying on various optimizations to achieve great results. However, this means that there is no guarantee that their results are correct. The easiest way to overcome that problem is to output formal verifiable proof, but it is still not standard for automated theorem provers. I will talk about how formal Coq proof output was achieved in the mSAT library for SAT solving, and in the archsat SMT solver which builds on mSAT.

14h45 - 15h : break

15h - 15h45 : Roberto Blanco (Inria & LIX)
Title: Translating between implicit and explicit versions of proof
The Foundational Proof Certificate (FPC) framework can be used to define the semantics of a wide range of proof evidence. An important decision in designing a proof certificate format is the choice of how many details are to be placed within certificates. Formats with fewer details are smaller and easier for theorem provers to output but they require more sophistication from checkers since checking will involve some proof reconstruction. Conversely, certificate formats containing many details are larger but are checkable by less sophisticated checkers. Since the FPC framework is based on well-established proof theory principles, proof certificates can be manipulated in meaningful ways. In this talk, I illustrate how it is possible to automate moving from implicit to explicit (elaboration) and from explicit to implicit (distillation) proof evidence via the proof checking of a pair of proof certificates. Performing elaboration makes it possible to transform a proof certificate with details missing into a certificate packed with enough details so that a simple kernel (without support for proof reconstruction) can check the elaborated certificate. We illustrate how trust in only a single, simple checker of explicitly described proofs can be used to provide trust in a range of theorem provers employing a range of proof structures. This talk is based on a paper that appeared in CADE 2017 and is joint work with Roberto Blanco and Zakaria Chihani.

15h45 - 16h30 : discussion

GT Upscale