A foundational approach to proof certificates: An application of proof theory to computer science
Dale Miller (INRIA Saclay & LIX/Ecole Polytechnique)
COMPUTER SCIENCE SEMINARDATE: 2013-05-14
TIME: 14:00:00 - 15:00:00
LOCATION: Engineering Lecture Theatre
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
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 provide an overview of a multi-year project that is designing a trustworthy proof checker that can check a range of proof structures (eg, natural deduction,resolution refutations, and proof nets) in classical and intuitionistic 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.
BIO:
Dale Miller received his PhD in Mathematics in 1983 from Carnegie Mellon University. He has been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and a department head at Pennsylvania State University. He has held visiting positions at the universities of Aix-Marseille, Sienna, Genoa, Pisa, and Edinburgh. He is currently Director of Research at INRIA-Saclay where he is the Scientific Leader of the Parsifal team. Miller is the Editor-in-Chief of the ACM Transactions on Computational Logic and has editorial duties on several other journals. He was awarded an ERC Advanced Investigator Grant in 2011 and is the recipient of the 2011 LICS Test-of-Time award for a paper he co-authored in LICS 1991. Miller works on various topics in the general area of computational logic,including automated reasoning, logic programming, proof theory,unification theory, operational semantics, and, most recently, proof certificates.
