The Coq mailing list

[Bai Wei <baiweiyj AT gmail.com>]

Hi. I mean if I have a proof of one theorem in Coq. Is it possible for me to check this proof using a standalone checker (not Coq itself)? Many thanks!

Regards,

Wei Bai

On Tue, Apr 23, 2013 at 4:55 PM, Beta Ziliani <beta AT mpi-sws.org> wrote:

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