coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?

From: Jonas Oberhauser <s9joober AT gmail.com>
To: Bai Wei <baiweiyj AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Does Coq proof checker can be used as a proof checker in Foundational PCC paradigm?
Date: Wed, 24 Apr 2013 14:27:46 +0200

Hi Wei Bai,

I only skimmed the paper FPCC by Appel, but IIRC the formulation that Appel gave in Twelf violates the non-negativity constraints of Coq.

I don't know if that helps.

Regards, Jonas

2013/4/24 Bai Wei <baiweiyj AT gmail.com>

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