The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

http://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/

On Thu, Mar 26, 2015 at 5:38 AM, Pierre Courtieu
<pierre.courtieu AT gmail.com>
 wrote:
> 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