coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Marco Servetto <marco.servetto AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 12:57:47 +1200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=marco.servetto AT gmail.com; spf=Pass smtp.mailfrom=marco.servetto AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f45.google.com
Ironport-phdr: 9a23:iM62kBL6bIbE9Gi9ctmcpTZWNBhigK39O0sv0rFitYgeL/TxwZ3uMQTl6Ol3ixeRBMOHsqwC0LOd6PCocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTuwbal8IRmrogncuMobipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPhcNwgqBUrhKvqRJ83oDafp2aOvVlc6PBZNMXX3ZNUtpNWyFDBI63cosBD/AGPeZdt4TzoEEBrQGiCgmrGejh1yFHhmXo3aIkz+QhDQbG1xEnEtILqnvUtsn6NKAIXeCu0qbI1yvDYO1K2Tfh74jFaR8hofSWUrJxdcrd01UgFwTAjliJr4HuIjya2PgXvWeB8+pgSfygi3QhqwxprDaix8khhIfGi48L1F3J6CV3zYIpKNC2R0B2YNCpHZpNui2GKYZ7QsMvTn11tCsn17ELpJ62cicKxZkk2hPSZPqKeJWG7BLkUeaeOzZ4hHR9db2jgBay606gxfP4VsmwylpFsDdKksTKu3sQ1BLT8tCKRuVh8kqlwzqC1ADe5vtaLUwpiabXMZEsz742m5EOq0rMBDX2l1/zjKKOdkUr5Oyo6+P/b7XjvJCcNot0hhj5MqQyh8CzGOo4PwcOUmSB9uS807rj/UL9QLpUlPE5jq7ZsJXCKcQaoK62HRNV35495xqjCzqqytcVkHkdIF5bZR6Lk5LlNl7OLfzgCPewmVWskDNlx/DcOb3hB43ALn3Zn7f7Ybl97FRQyBEtwtBF+ZJbFK0BIO70WkLqu9zYCwU2Mw2ww+r9FNp90YYeVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3VaFSHtYY2u4d6M6/DAyToy8XqnZQYX4pbWb1yDzJZBMeG1aFlfERXLhbY6DHewBcjyfPtNmujMBXLmlDYQm0Ef950fB17N7I7+MqWUjvpX52Y0tvrGBpVQJ7TVxSv+l/SSVVWgtxzEHQjY32OZ0pkkvkg7Sg5g9uORREJlo390MVw47MZDGyOkjUoL9XwvAepGCT1P0G4z7UwF0dco4xpo1W2g4G9imiUqejS+jArtQkKDSQZJor+TT2H/+I8s7wHHDhvEs

Well, the issue here is more complex, because the proof must contain
the full representation of the C code
(I said "must" but I have no proof of such statement, and I would love
to be shown wrong)

On Wed, 15 Jul 2020 at 12:53, Kevin Sullivan <sullivan.kevinj AT gmail.com>
wrote:
>
> Is an essay about War and Peace a derivative work? This isn't legal advice,
> but that's what I'd argue. Such a proposition and proof is an independent
> statement (supported by evidence) about an existing work. The more
> interesting question is whether such a proposition and proof is derivative
> of the program's specification (ha ha, as if it really has one).
>
> Kevin Sullivan, UVa
>
> On Tue, Jul 14, 2020 at 8:40 PM Abhishek Anand
> <abhishek.anand.iitg AT gmail.com> wrote:
>>
>> For licensing purposes, is a Coq proof of correctness of some C code
>> considered a derivative of the code?
>> Any experience/advice/opinion will be appreciated and won't be considered
>> formal legal advice.
>>
>> Thanks,
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/

[Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/15/2020
- Re: [Coq-Club] license: derivative status of proofs, Kevin Sullivan, 07/15/2020
  - Re: [Coq-Club] license: derivative status of proofs, Marco Servetto, 07/15/2020
    - Re: [Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/15/2020
      - Re: [Coq-Club] license: derivative status of proofs, Tej Chajed, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Jim Fehrle, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Kevin Sullivan, 07/15/2020
        Re: [Coq-Club] license: derivative status of proofs, Izzy Hasson, 07/15/2020
        Re: [Coq-Club] license: derivative status of proofs, Jim Fehrle, 07/15/2020
        Re: [Coq-Club] license: derivative status of proofs, Abhishek Anand, 07/16/2020
        Re: [Coq-Club] license: derivative status of proofs, jonikelee AT gmail.com, 07/16/2020
        Re: [Coq-Club] license: derivative status of proofs, Jim Fehrle, 07/16/2020