coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Bai Wei <baiweiyj AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?
Date: Wed, 24 Apr 2013 18:35:23 +0800

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

[Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Bai Wei, 04/24/2013
- Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Jonas Oberhauser, 04/24/2013
- Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Adam Chlipala, 04/24/2013
- Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Duckki Oe, 04/24/2013
  - Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Bai Wei, 04/28/2013
- Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Amy Felty, 04/25/2013
- Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Amy Felty, 04/28/2013
  - Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?, Gabriel Scherer, 04/29/2013