The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

The paper should imho:

1) Allow the reader to be convinced that the coq definitions do really
model the notions you pretend. The necessary amount of sub-definitions
needed for this depends on the number of "new" formalization layers
you are using. For example describing extensively already
well-established definitions/libraries is pointless (refer to the 
corresponding
papers instead).

2) Allow the reader to be convinced that the final(s) theorem(s)
statement(s) do really correspond to the one(s) you claim. This should
be easy if 1) is OK.

3) Refer to the real Coq development, which should be put somewhere on
the web, preferably for a long time (years).

The verification task (that a referee should perform at least) is to
download the coq files, compile them and check that the theorems are
the same than in your paper and do really use the definitions
described in the paper. This last step should be performed in Coq with
commands like Print/Check/Set Prinitng All etc. Checking the files
without running/querying Coq should not be considered enough since for
example a small notation can drastically modify the meaning of a
definition, without being spotted.

My two cents,
Pierre

2015-03-23 17:41 GMT+01:00 George Van Treeck 
<treeck AT yahoo.com>:
> I'm a software engineer and could use some advice from real mathematicians
> on how Coq proofs should be included with an AMS journal article.
> I have written a article with less formal proofs for human consumption
> paired with Coq-based proofs for machine consumption.
> Without Coq-based proofs the paper is only 10 pages, with Coq-based about 40
> pages.
>
> Being as Coq-based proofs are only intelligible at best by the Coq-literate,
> is the normal practice to:
>
> a) Include long Coq-based proofs directly in article text?
> b) Place long Coq-based proofs in an appendix?
> c) Put a URL reference to the long Coq-based proofs in the text? If so, then
> where on the internet should the proofs be uploaded? As *.v files?
>
> -George