coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Cc: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 20:03:27 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f177.google.com
Ironport-phdr: 9a23:ZIteghHtUSGuSC1Mc7DCQJ1GYnF86YWxBRYc798ds5kLTJ7zpM6wAkXT6L1XgUPTWs2DsrQY0rSQ6PurBzdIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLJ/IA+4oAjfucUbgIVvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFog61brhCuqRxxzYDXfY+bKuZxc7jHct8GX2dMRNpdWzBDD466coABD/ABPeFdr4Tlo1UOrB6+DhSsCuzxyj9InHv20rMn2OkmEwHG3QkgE8gAsHvKrNX1LqMSXv6uwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesXe1UchDRnKjkmMqYP7JTOV0PwAv3aG4+dgSO6ilWoqpQ5/rzWvyMkihYnEi4Ybx1zZ9Sh3z4U4KcCkRUN4ZdOpDJpduiWeOoV2Tc0vTX9ltSI1xLAApJW1ci8KyJE9yB7ebfyKa5SH4hX7VOeRJTd3mnxleK6lixa160igxevxXdS33lZStidJjMXAu3QX2xHQ6sWLUOZx80ag1DqVygze6ONJLEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2gbeTdko+++io7/3rYrTippOBLoN0hBzyP6Ysl8ClDuQ4NQ8OX2ef+euizrHs4Ur5QLBSgv03lKnWrozaKNwFqqKlBwJZyIUu5halAzu70dkVnGMLIE9HdR+Fl4TpPkvBIPH8DfexmVSslzJryujEPr3gB5XBNHbDn6nhfbZn705T1hE+zd9a551OC7EBJOj/VVP2tNzdFhM5KRC7w/77CNVh0YMTQX6AAqiAMK/LrVCI4v8vLPKXaY8OuDf9LuAl6OT0gX84n18dZ6ip0oENZHC2BPQ1a3meNHHrm5IKFXoAlgs4Vu3jzlOYAhBJYHPnfaM5rh82CJiiAM+XRIGoxrKM3D2/E7VZY2lHDhaHFnK+JNbMYOsFdC/HepwpqTcDT7X0E9Z9hyHrjxfzzv9cFsSR4jcR7Mux29185umVnhY3p2QtUpatllqVRmQxpVsmAj872Kcl/x54w1aHlKl82rlWTIMMofxOVQg+ONjXyOkoU4mjCDKERc+ATROdevvjBDgwStwrxNpXOhRyHtyjilbI2C/4WrI=

> The C code is available publically under GPLv2 license.

You could ask copyleft.org for their opinion on your situation. Or maybe it's Free Software Foundation or Software Freedom Conservancy. That may be the safest, most conservative approach though there is a risk they might say "no".

On Wed, Jul 15, 2020 at 7:04 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Wed, 15 Jul 2020 18:36:51 -0700
Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> On Wed, Jul 15, 2020 at 1:45 PM Jim Fehrle <jim.fehrle AT gmail.com>
> wrote:
>
> > 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).

Found this, which may be relevant:
https://copyleft.org/guide/comprehensive-gpl-guidech5.html

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