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: Stefan Monnier <monnier AT iro.umontreal.ca>, Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 21:52:42 -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-io1-f45.google.com
Ironport-phdr: 9a23:rc6Q4Re7GfDiOivZLeX0i5awlGMj4u6mDksu8pMizoh2WeGdxcS4YR7h7PlgxGXEQZ/co6odzbaP7ea7AidQv96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLRi6twvcu8cZjYZhK6s61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuUOM+ZXrYnzqVUNoxWjGwejGPjixSVUinLsx6A2z/gtHAPA0Qc9H9wOqnPUrNDtOakWUOC1ybTDwzXdYPNWwzf97JbHeQ0mrPGOXLJwdNDdyUcxGAPFlFWQrZLqMiia1uQIqWeb7u5gWfizhG4grgF8uz6izdojhYfVnIwa0EzE9Tlnz4YvI921UFJ2bN26HZZUuCyXNo97T8E+T2x2tig3zqEKtIK/cSQWyZkqyR/SZuKZfoSU5h/uUOScLDh2in94d7yymgi//VSmx+bhVce0yE5HojRZntTIrHwA1Bze5tKaRvZ8/0qtwzmC2gDV5+pZO047j7DbJIQkwrMolpocr0DDHijulUXzlqCWd0Ek9vGp6+Tgf7nqv5GcOoB0hw3kPaQuncu/Aes8MgcQRWSU5eO81Lj78U34RrVFkOE2n7HHvJzGIckXvK20Dg9P3oo+6huyDi2q3dsYkHUfKVJKYhOHj4znO1HUJ/D4CO+yg1atkDdu3fzGMKPuApXXLnjHjrjsZrl960tGxwoyydBT/Y5bCrYEIP7rQE/+qMTYDgMlMwyz2+voFNJ91poHVW2TBq+ZLbjdvEST5uMvJumMfJUatCz8K/gj/f7ujGU2lUUTfamzjtMrbyWzGe0jKEGEa1LthM0AGCEEpFkQVuvv3X+DVHZ9anaoW690sjM6DcSoAIfZQo2Fj7mI3SP9FZpTMDMVQmuQGGvlIt3XE8wHbzifd4o4ymRdCeqRDrQ53BTrjzfUjqJ9J7ONqCIdvJPnktNy4r+LzEBgxXlPF82Yllq1YSRxl2IMSSUx2fkm80N4w1aHl6N/hq4BTIEB17ZySg4/cKXk4al6BtT1AF+Te96ITBOnRYzjD21sCN02xNAKbgB2HNDw1h0=

If you write new code with the same functionality as the original, copyright protection may not apply because copyright only covers the form of the _expression_. That's how FSF and Linux were able to duplicate Unix. This defense is most persuasive when the author of the new code never looks at the original code, instead working from specifications prepared by others. You would also need to avoid patents and trade secrets used to create the original, though I expect anything in open source can't have trade secrets. The original authors probably have to grant a license to any of their patents used in the code, which the GPL would then sublicense to others. Third party patents could still be an issue. e.g. the original code could infringe a third party patent, a problem that the new code could inherit.

My understanding of US law. I'm not a lawyer.

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