coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Tue, 14 Jul 2020 20:53:15 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f51.google.com
Ironport-phdr: 9a23:01xOLR/0KNrBBP9uRHKM819IXTAuvvDOBiVQ1KB31escTK2v8tzYMVDF4r011RmVBNudsKsP0LeempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgRFiCCzbL9vIxm7owXcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh/27XhM5/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZOOhXsZf9p1oIrRCjGAesGefvyjtJhn/ox6I61fkqHAbd3Aw9G9IOtHXUrMvvO6cUS+y1z7fHzSvCb/NQ2zfw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtIPqMS+P2OsXr2ib8/RvVfipi2M/pQ99vzihyMcih4fJm44YxVDJ+yVnzYorJNC1R052bN2kHpdOuCyUN5Z6T8I+Tmxmtyg2170LtYK0ciUJx5opyRjSYOGJfYiP5xLsTueRITFgiX15f7K/nRCy/lakyu34TMW7zktFrjdDn9LRtX4NzwTe5tabRvZ55Eus2jaC2xrN5u1YIk04j6rWJ4Mnz7UtjJQcq17DETXzmEjujK+ZaEEk+u+w5uTieLrmp5ucO5ZqhQ7jL6gig8K/DOQlPgQUUGib/uO81LLn/ULnWrlFkvo2kqzBvJDbI8QUuLK5DhdL3oo/7xuzFTSr3dQCkXUZMF5IewiLgoj0N13WJfD3F/a/g1CikDdxwPDGO6XsAo7QLnjHlLfhfKh95FRayAYpztBQ+YxUCrAHIPLxQULxu9nYAQU4Mwyw2eroFNJ91oYGVWKVHqCZKL/SsUOP5u83P+aMY5YVtC/hJPgh+v7hlmQ0mUQdfKmsxZsYcmq0HvVgI0WDYHrjmM0NEWkQvll2cOu/g1qbFDVXenyaXqQm5zh9Bpj1I53EQ9WOjaKA2m+AA5lSZ35PDBjYCmrsc4SaUvFKay+MI8ljujMBXLmlDYQm0Ef950fB17N7I7+MqWUjvpX52Y0tvryBpVQJ7TVxSv+l/SSIRmBwkHkPQmZvjq96qE15jFyE1Poh2qEKJZlo//pMFzwCG9vcwuh9UY2gXwvAepKERA/jTIj/Rz42Sd01zpkFZEMvQ4z+3CCG5DKjBvour5LOHIY9q/uO0H34JsI7wHHDhvEs

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