The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

Hi, 

After you extract the raw proof term from your Ltac script (to check with 
Coq's kernel), you will also need to extract all the definitions that your 
proof may use from the standard library and distribute them as your theory as 
well. I don't know if there are any tools to automate this process. If you 
really want to use Coq (with tactics) as a proof generator. This will be the 
only way to do it. It will be certainly harder to translate Coq terms into 
simpler type theories like LF (twelf) than the other way around.

If you can use other proof generators (like SAT/SMT solvers), there are more 
options because SAT/SMT are smaller fixed logics and they have been encoded 
in several different proof systems.

-- Duckki



On Wednesday, April 24, 2013 at 6:35 AM, Bai Wei wrote:

> Hi. I want to implement Foundatinal proof carrying code (FPCC) paradigm. 
> Does Coq proof checker can be used as a proof checker in FPCC? Many Thanks!
> 
> Cheers,
> 
> Wei Bai