coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Xuanrui Qi <xuanrui AT nagoya-u.jp>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 11:14:30 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xuanrui AT nagoya-u.jp; spf=Pass smtp.mailfrom=xuanrui AT nagoya-u.jp; spf=None smtp.helo=postmaster AT smtp.nagoya-u.jp
Ironport-phdr: 9a23:EQO0fBHOA0owZoFYqq9KPJ1GYnF86YWxBRYc798ds5kLTJ7zr86wAkXT6L1XgUPTWs2DsrQY0rSQ6PmrBDFIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLJ/IA+4oAnMucUbgYtvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jygJKSA28W7LisJpiqJbpBKgqwVmz4PIboyYNvRzcrrBcd4VWGFNWsZcWzBEDo66coABDfcOPfxAoof+ulUArQWwCweuC+Ph1jBHiHD506Ih3uQ9EwzLxhAsE84UvXnWqtj+KaccUfqyzKnN1TjMbu5W1i376IjSbxAhoOyHU6lxccHMzkQuGB7FgU+WqYz/IjOV1/8As26B4OpvUuKui3QopxhsojS1xMcskpDEi4QIwV/L6St32pw6JcGkSEFle96kFoNduiKaOYZ2Tc0sQ2VltDokxrAapZO1czQGxYopyhLCa/KKfIaG7w7jWuufLjp0mXBodbGhihi9/katxPPwW8uq3FtMsyFLnN7MtnUX2BzS7MiKUudy/kC72TaJyQ/T7uVELVoqmqXGNp4sxKM7mJkLsUnbAyP7lkv7gLWXe0k+5+Sl6Prrbq/lq5KSL4N4lxzyP6Q0lsGxAuk0KBUCUmqG9eimybHu/k70TbNXhfMsiKbZqorVJcEDq665HQBV1oEj5g6kDzejzNQYhWMLLFRfdxKIiIjoO0vBLOnlDfulgVSsiC9nx/HAPrL/HpXANmXPnbnvcLpn6kNQ0hc/wNNB655OCbwMLur/Wkrru9zZCh85PRa0w+HiCNhl2YIeRHiAAqmDMKPPsF+F/eQvLPODZI8SuDfyMeEp5+P0gX87gV8RZbOp0ocPaHCkAvRmJF2UbmbrgtcYCGsFog4+TPHxh1CZSj5SZ3OyX7om6T0hCYKmC53DRoG3j7Cb0ie7BM4eWmcTAVeVVHzsao+sWvEWaSvULNUyvCYDUO2RVoYnzwyv/Db7g+53M+PS4DAZnZTq299k7qjO0xMqo28nR/+B2n2AGjkn1lgDQCU7if0n+B0v+hK4yaF9xsdgO5lW7vJNXB09MMeHnepzBNfjU0fcONWRGg//H4eWRAopR9d0+OcgJkZwH9L73kLY2jayRbkcmLuaDdkptKDEjSCoe5RNjk3e3axktGEIB9NVPDT91Kh2+A/CDsvU1UeBxf6n

Hello all,

I believe this issue is likely very subtle and will perhaps require
consultation with a professional IP attorney.

An answer to this question would require scrutiny of the wording of the
original license, and some knowledge of the related legislated and/or
case law (if in a common law jurisdiction).

But I suspect the situation is somewhat similar to ZFS on Linux...

-Xuanrui

On Tue, 2020-07-14 at 17:38 -0700, Abhishek Anand 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/

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