The rules of pCIC

[Christian Doczkal]

Hello

I have been looking on the web without success. Is there any paper /
tech report that gives the precise rules of the pCIC as it is currently
implemented in Coq 8.2. (something like a latex version of Chapter 4
from the reference manual)


--
Regards
Christian Doczkal

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Denis Cousineau]

Hi Christian,
I am not sure that it answers your question but there exists a pdf  
version of the reference manual: http://coq.inria.fr/distrib/V8.1pl5/files/Tutorial.pdf

Denis


--
Denis Cousineau
http://www.denis.cousineau.eu





--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[hugo.herbelin]

Hi,

> I have been looking on the web without success. Is there any paper /
> tech report that gives the precise rules of the pCIC as it is currently
> implemented in Coq 8.2. (something like a latex version of Chapter 4
> from the reference manual)

There is a latex version of the reference manual in the Coq source
archive and a pdf version at http://coq.inria.fr/distrib/V8.2pl1/files/.

AFAIK there is no other description on paper of the entire set of
features of pCIC in its 8.2 implementation. Note however that there is
a work in progress by Gyesik Lee and Benjamin Werner on the
set-theoretical model of a formulation of pCIC that is very close to
Coq.

Hugo Herbelin

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Andrej Bauer]

On Mon, Nov 2, 2009 at 9:44 PM,  <hugo.herbelin@...> wrote:
> AFAIK there is no other description on paper of the entire set of
> features of pCIC in its 8.2 implementation.

This is somewhat interesting. What would you say is the reason? Is it
a software-engineering problem? From a philosophical point of view
this is a bit worrying. I suppose from a practical point of view it
allows Coq to develop more rapidly.

Andrej

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club