19
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Checking Zenon Modulo Proofs in Dedukti

      Preprint
      ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Dedukti has been proposed as a universal proof checker. It is a logical framework based on the lambda Pi calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs produced by Zenon Modulo, an extension of the tableau-based first-order theorem prover Zenon to deduction modulo and typing. Zenon Modulo is applied to the verification of programs in both academic and industrial projects. The purpose of our embedding is to increase the confidence in automatically generated proofs by separating untrusted proof search from trusted proof verification.

          Related collections

          Author and article information

          Journal
          30 July 2015
          Article
          10.4204/EPTCS.186.7
          1507.08719
          12050fa3-73c0-487b-91de-6cd0e23d00dc

          http://arxiv.org/licenses/nonexclusive-distrib/1.0/

          History
          Custom metadata
          EPTCS 186, 2015, pp. 57-73
          In Proceedings PxTP 2015, arXiv:1507.08375
          cs.LO
          EPTCS

          Comments

          Comment on this article