Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Jim Fehrle <jim.fehrle AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] license: derivative status of proofs
  • Date: Wed, 15 Jul 2020 13:44:59 -0700
  • Authentication-results: mail3-smtp-sop.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-f178.google.com
  • Ironport-phdr: 9a23:FrBS1RJpWd0BNtqI89mcpTZWNBhigK39O0sv0rFitYgRI//xwZ3uMQTl6Ol3ixeRBMOHsqwC0LCd6v28EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe8bL9oIhi6swrdutQWjIZtN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9g61VoB2jpxJxzY3abpyLOvViZa7SZ88WSHBbU8pNSyBMAIWxZJYPAeobOuZYqpHwqV8PrRu7GAKiBP3gyj9Shn/yw6IxzuMsEQPH3AwlBd4OvmrbrNXvNKcWT++416bIzTDZYPNX3Tfx8pTHchckofyVW797bMXex1U1GQzfklWQtZLqPymT1ukVr2WW7PRtWOaghmMmrwx8oCSjy9kihITNmo4Y1lTJ+Tl4zYs7JNC1VlB2bcKgHZZUtSyXOIV4T94tTWx1pis21rsLsoO4cigS0Jkr2QLTZvidf4WL4h/vTvudLDZ5iX5/Zb6yhRW//E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CCSvRn/0eh3S+D1wHX6u1ZOEw0m7fXJpwiz7IqmZoTtkPDHiDymErolqOZakIk+u2w5+TmZLXpuIOcOpdqhg3iNqkigM+yDOQiPgQTXmWW+P6w2KDh8ED6WLlKi+c5kqjdsJDUP8Qboau5DhdX0oYi7hazFTmm38oYnXkdKFJKZgmKj4fsO17UIfD4Ce2zjEirkDdu3/zGJKHuAo3RLnjfl7fsZapy60lFyAYq0d9f449UBaoaLfLoWk7xscTYAQUjPwy1xebnEtR92ZkEVWKBGK/KeJ/V5FSP/6ckJ/SGTI4Tojf0bfY/tND0inpsu14YNYek3YETZTjsHPVjZUuUYWDoj/8OFG4Lukw1S+m82w7KaiJae3vnB/F03To8Eo/zVd6fFLDou6SI2WKAJrMTfnpPUwneHnLhdoHCUPAJOnrLf51R1wccXL3kcLcPkBGjsAiglehiJ+vQvywc7NftjYcloeLUkh42+Hp/CMHPizjcHVExpXsBQnoN5I46pEV8zlmZ1q0h2q5XENVS47VCVQJobJM=

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.

On Wed, Jul 15, 2020 at 12:51 PM Izzy Hasson <izzyjhasson AT gmail.com> wrote:
The issue with the question of whether a proof of correctness of C code is considered a derivative of the code from an IP/licensing/legal perspective is kind of incomplete. There are three sets of laws, I can think of, in the US that could be relevant, Patent, Copyright, and Contract, and each can yield different conclusions. With Patents ,assuming the code somehow had a valid patent attached to it, I can't imagine how the proof of code would be considered a derivative of the code and I don't think whether or not the proof contained a verbatim reproduction of the code would matter. With Copyright I can't think of how the proof of code wouldn't be a derivative of the code but you have fair use considerations which could render the question of derivation irrelevant. Finally with Contract law I have no clue.

Sincerely,
Some guy who is definitely NOT a lawyer



Archive powered by MHonArc 2.6.19+.

Top of Page