coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] license: derivative status of proofs

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 23:12:37 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
Ironport-phdr: 9a23:wkzmsB+O8CurPf9uRHKM819IXTAuvvDOBiVQ1KB32+kcTK2v8tzYMVDF4r011RmVBNudsKkP1bGempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgRFiCCzbL58Ixm7rAvcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh8G/ZlNF+gqFVoByvpRNwzYHbb52OOfpiYq/QZ88WSXZbU8pNUSFKH4Oyb5EID+oEJetWspX9qEUArRSkAwmnGeThyjhOhn/w3K01zf4hGhzB0QwlGNIOtnLUrNTrO6cISu21zbPIzTLZY/NL3Df9747Icgw7of6SR71wddDdxlU1GA7ciFibtIPqMS+P2OsXr2ib8/RvVfipi2M/pAx8ozihytojhITKiIwYyV7J+Dl2zog6KtO1S1N3bcOlHZdMuC+XKYp7T80gTmx2uys3zqELtJC7cSYKyJkqxRjSYOGEfYiQ+h/vSeicLSliiH57ZL6yiAy+/Vagx+HmVsS4zE5GoyVFn9XWtH0ByQbf5tWZRvZ55Eus1iiD2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmErsja+Wcl4k9fSy5OThZLXpuIWcO5V1igHkNaQigNG/AeE/MggIQ2ib4/qz26fn/UHjXLpFlOU6kqjfsJ/EOcQWvrO1DgFL3oo59RqzEzir3M4GkXQHNl5IeA6Lg5DsO17UIfD4Cfm/g06rkDdu3/3GO7rhApPLLnjCjrjhZ61w609GyAo019xf+pdUCrYHIPLvQE/+qsbXDhsjPwOo2enrEM992Z8GWWKTHq+ZN7vfvkOP5uI2OuWDeIsVuCvmJPU+/P7vjXo5mUcHcqWz3JsXbmq4HvV8LEmDb3rsmIRJLWBflwA+TffqhV7KeDhaYXr6C6s25jAgCI+lS47FT4ahxr2AwCiTEZhfZ2QAAVeJRyTGbYKBDswQZSybJIdElToCVLW7A9sk0heotQLg47t9KazJ/yoeqYju3dwz7OSFxkJ6ziB9E8nIizLFdGpzhG5dH2ZrjpA6mlR0zxK46YY9g/FcEocLtfZAUwMhPpfayeFgTdHoXUTce9CPVEyrS9HgCjhjFotgke9LWF50HpCZtj6G2iOrB7EPkLnSVM416KWawn32Idpnxn/CkqIo3QB/Hpl/cFa+j6s6zDD9QpbTmhzJxaewcuIB2SnL6H2OxG7It0gKCAM=

>> Another approach would be to ask the owner of the C code whether they have
>> any objection to your publishing the proof. Seems to me your proving it
>> would make their code more valuable.
> The C code is available publically under GPLv2 license. The main question
> is whether the correctness proof (just the .v file(s) containing the specs
> and proofs, NOT the code or the .v file containing the code AST) can be
> released under a different license (possibly incompatible with GPLv2).

I'm not sure what there could be to gain from using an incompatible
license, but Jim's approach is still relevant anyway: ask the author(s).
If they're OK with it, then you don't need to figure out what the law says.

Stefan

Re: [Coq-Club] license: derivative status of proofs, (continued)
- Re: [Coq-Club] license: derivative status of proofs, Xuanrui Qi, 07/15/2020