Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Fri 28 Sep 2018 13:55 - 14:20 at New York Central - Session 2

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 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:30 - 15:10
Session 2ML at New York Central
13:30
25m
Talk
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
25m
Talk
Design and verification of functional proof checkers
ML
14:20
25m
Talk
Disornamentation
ML
14:45
25m
Talk
Generic Programming with Combinators and Objects
ML