The Coq mailing list

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

Then you should look at the xml-export interface, I suppose:

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual017.html#sec595



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