The Coq mailing list

[George Van Treeck <treeck AT yahoo.com>]

Thank you! That was very helpful, Yves.

-George

On Wednesday, March 25, 2015 9:25 AM, bertot <Yves.Bertot AT inria.fr> wrote:

On 23/3/15 5:41 PM, George Van Treeck wrote:

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

I am more into computer science myself, but here are my two cents.  You often can submit preliminary versions of your papers in preprint archives, and provide the Coq files as ancillary files.  An example is the following paper by Pelayo, Voevodsky, and Warren:

http://arxiv.org/abs/1302.1207

Then the published paper can still refer to the Coq sources associated the preprint, I think.

In france, we also use the hal open archive for this purpose.

https://hal.archives-ouvertes.fr/

This archive also allows to attach auxiliary files to the papers, Here is an example:

https://hal.inria.fr/hal-01074927

Yves