A foundational approach to proof certificates

Feb 22, 2013 | 02:00 PM c.t.


Dale Miller, Director of Research at INRIA Saclay - Île-de-France and the Laboratoire d'Informatique (LIX). Team leader of Parsifal

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 overview some recent work on designing a trustworthy proof checker that is able to check a range of proof structures (eg, natural deduction, resolution refutations, and proof nets) in classical, intuitionistic, and linear logics. I will also describe various future directions for this effort, including building marketplaces and libraries for proofs and developing ways to check and use partial proofs and counterexamples.

Time & Location

Feb 22, 2013 | 02:00 PM c.t.

Takustr. 9, SR 005. Ab 13:45 Uhr Kaffee mit dem Vortragenden im Raum 137