The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi,

I'm not sure if I understand your question. Have you checked the
extraction mechanism in Coq?

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual025.html


On Tue, Apr 23, 2013 at 10:47 AM, Bai Wei 
<baiweiyj AT gmail.com>
 wrote:
> 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