The Coq Users' Contributions

Coq is used in a large variety of domains such as formalization of mathematics, specification and verification of computer programs, etc.

Submitting your Coq development as a contribution provides visibility to your work and the ensurance to have it maintained and made compatible with the forthcoming versions of Coq. For the Coq developers, it helps to evaluate the robustness and efficiency of the evolutions of Coq.

In order to make your contribution available from the Coq web site, we expect you to select a license that allows us to redistribute it and to keep it compatible with the new versions of Coq. Some hints on how to choose a licence are given here.