coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Extract proof checker for a specific proof

From: Bai Wei <baiweiyj AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Extract proof checker for a specific proof
Date: Tue, 23 Apr 2013 16:47:13 +0800

Hi! I have write a proof in Coq and I want to extract a standalone proof checker to check this proof by implementing Proof Carrying Code(PCC) paradigm. Is it poosible to extract a proof checker that is just used to check this proof?

Cheers,

Wei Bai

[Coq-Club] Extract proof checker for a specific proof, Bai Wei, 04/23/2013
- Re: [Coq-Club] Extract proof checker for a specific proof, Beta Ziliani, 04/23/2013
  - Re: [Coq-Club] Extract proof checker for a specific proof, Bai Wei, 04/23/2013
    - Re: [Coq-Club] Extract proof checker for a specific proof, Beta Ziliani, 04/23/2013
    - Re: [Coq-Club] Extract proof checker for a specific proof, Frédéric Besson, 04/23/2013