EasyChair Publications
Search
Paper Information
Paper:Zakaria Chihani, Dale Miller and Fabien Renaud
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
Title:Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
Authors:Zakaria Chihani, Dale Miller and Fabien Renaud
Keyphrases:proof checking, certificates, proof theory
Paper:
Abstract:We present the design philosophy of a proof checker based on a notion of foundational proof certificates. At the heart of this design is a semantics of proof evidence that arises from recent advances in the theory of proofs for classical and intuitionistic logic. That semantics is then performed by a (higher-order) logic program: successful performance means that a formal proof of a theorem has been found. We describe how the lambda Prolog programming language provides several features that help guarantee such a soundness claim. Some of these features (such as strong typing, abstract datatypes, and higher-order programming) were features of the ML programming language when it was first proposed as a proof checker for LCF. Other features of lambda Prolog (such as support for bindings, substitution, and backtracking search) turn out to be equally important for describing and checking the proof evidence encoded in proof certificates. Since trusting our proof checker requires trusting a programming language implementation, we discuss various avenues for enhancing one's trust of such a checker.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:58-66
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:8
Downloads:7
BibTeX entry:
@inproceedings{PxTP2013:Checking_Foundational_Proof_Certificates_for_First-Order_Logic_Extended_Abstract,
  author    = {Zakaria Chihani and Dale Miller and Fabien Renaud},
  title     = {Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {58-66},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}