Skip to Main content Skip to Navigation
Conference papers

Checking Zenon Modulo Proofs in Dedukti

Abstract : Dedukti has been proposed as a universal proof checker. It is a logical framework based on the λΠ-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.
Keywords : Proof Checking
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Pierre Halmagrand Connect in order to contact the contributor
Submitted on : Friday, July 3, 2015 - 2:34:35 PM
Last modification on : Friday, January 21, 2022 - 3:15:39 AM
Long-term archiving on: : Tuesday, April 25, 2017 - 11:37:10 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License


  • HAL Id : hal-01171360, version 1



Raphaël Cauderlier, Pierre Halmagrand. Checking Zenon Modulo Proofs in Dedukti. Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany. ⟨hal-01171360⟩



Les métriques sont temporairement indisponibles