Coq Users' Contribution Licensing HOWTO

Coq developments have a rather specific status.

• As theories made of definitions, theorems and proofs, they can be seen as mathematical developments and henceforth liable to contribute to the process of construction of a universal corpus of scientific knowledge, following a long-established scientific tradition of public diffusion and credits' acknowledgments.
• Coq developments may contain programs and also proofs of which programs can be automatically extracted. As such, Coq developments are liable to be equipped with licenses used for softwares, including open source licenses such as the GPL or the BSD licenses, or proprietary licenses from which commercial benefits is generally expected.
• Coq developments may have a role of software certification, where, again, open source licenses or proprietary licenses with commercial aims can be considered.

Since any development of yours is liable to be used or extended with possibly different objectives than you had yourself, it is relevant to anticipate what kind of uses of your work you would like to allow or offer. It is not clear that existing licenses fully covers the typical aspects of a Coq development but here are some hints:

• If you wish that any released work that uses or modifies your contribution, e.g. to build a software or to certify properties of a software, be released together with its full source code and proofs (in Coq or in another language) so that other users can take benefit of it at their turn, then the GPL, or its French equivalent, the Cecill, may be a not too bad approximation of what you are looking for.
• If you wish that any work that uses your development (without modifying it), e.g. to build a software that links to code extracted from your development or to certify a software that depends on theorems formalized by you (relying on an independent accredited organism for authentifying the certification proofs), then a LGPL, or its French equivalent, the Cecill-C, may provide an approximation of what you are looking for.
• If you do not wish to impose any restriction or obligation to what can be done of your work (to the exception of citation), then a BSD license or its French equivalent, the Cecill-B may be appropriated.
• If ever you do not want to see the possible applications of your work to software engineering and just want to see it as a pure creation of mind, then an Open Publication License may be convenient for you. Check also for Creative Commons which provides a collection of licenses articulated around the following notions: attribution or not, commercial use allowed without former agreement or not, derivative works allowed or not, and if allowed with the same license or not.

Note that the standard library of Coq adopted the LGPL what possibly allows users wishing to use the library without having the obligation of releasing the source of their own developments to do so.

Note also that the compiled ".vo" files can be easily reverse-engineered. The original structure of the source file and the identifiers names are still there and only the comments are basically forgotten.

In any cases, all licenses cited above will permit the distribution of your work on our server and its adaptation to the new versions of Coq.