The Coq mailing list

[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