The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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)

Highly automated proofs often do not contain the representation of the code. The Ltac proof scripts are often just algorithms that find the concrete proof, when applied to the concrete Coq AST representation of the C code, the latter need not be distributed with the Ltac proof scripts. 

 

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/