The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/24/2013 06: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!

There's a good chance that the answer is "yes."  Certainly several 
research groups are using Coq in that way, though I don't know if 
anyone's bothering to check proofs with the minimized Coq checker 
regularly.  If you have more specific requirements, you might get a 
better response after sharing them.