Design and verification of functional proof checkers
Small proof checkers increase trust in the results of theorem provers by providing independent and trustworthy validation of results; even more, these checkers can be carefully architected to be reusable across proof formats and enable the communication and sharing between systems of proofs and their meaning. One such architecture is the FPC framework, based on sequent calculi for various logics, notably classical and intuitionistic. We describe purely functional implementations of determinate proof-checking kernels in OCaml and Gallina, and correctness of the latter is given by a formal proof of soundness in Coq, from which a verified checker can be extracted; we also discuss the integration of these tools in the context of general, not necessary determinate proof checking, and directly within proof assistants.
Fri 28 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:30 - 15:10 | |||
13:30 25mTalk | ML as a Tactic Language, Again ML Guido Martínez CIFASIS-CONICET, Argentina, Danel Ahman University of Ljubljana, Victor Dumitrescu , Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Cătălin Hriţcu Inria Paris, Monal Narasimhamurthy , Zoe Paraskevopoulou Princeton University, Clément Pit-Claudel MIT CSAIL, Jonathan Protzenko Microsoft Research, Redmond, Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research File Attached | ||
13:55 25mTalk | Design and verification of functional proof checkers ML Roberto Blanco Inria | ||
14:20 25mTalk | Disornamentation ML | ||
14:45 25mTalk | Generic Programming with Combinators and Objects ML |