coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 18:36:51 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f51.google.com
Ironport-phdr: 9a23:NWHNDxyIWNfRJX3XCy+O+j09IxM/srCxBDY+r6Qd2+8UIJqq85mqBkHD//Il1AaPAdyFrakfwLaL+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhJiTanb75/Ihq6oArRu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406G7YisJyg6xbrhyvpAFxzZDIb4yOLvVyYrnQcMkGSWZdXMtcUTFKDIOmb4sICuoMJfpVoJL9p1sPthu+BRejBODywTJUgH/5x6s63Pk8GgzBxgMvBNIOsHXPrNX1KqgSUvq5w7POzTrZafNZxC3x6InJchA9rvGBRr1wcc/LxkkuEwPJlEmfqYvgPz6M0OkGrmeU4fZ6W+21l24ntx9+oiKpxso0hYfHiJwYxF7Y+ShkwYs5O9y1RUF6bNO4DJZduSGUOYRyT80tQmxmtyk3xqEbtZO/YSUHyJcqygDeZvGFbYWF4RTuX/uSLzdgnH9pZq6zihKo/UWjyuDwTNS43VdLoyZfktTAq3YA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5la/BJJ4gxr48j5sTsUPeEiPvlkX7jLKael8r+uiv7OTnbbHmqYGGO4BojQH+N7wims25AesmLggDR3aX9fi42bH5/kD0QK9GguA3n6TYqpzXJdkXqra8AwBP04Yj7xi/Dy2h0NQdhXQINklKeBKGj4jyO1HBPvP4Ae2ljFSqijhrwe3JMqfgApXMMnjDn6zsfbl460FGyQozycpT6I5TCrEEOP7zQFP+tMTEDh8lNAy52/roCNJk1o8HRW2PBrKZP7jJvF+T5uMvJvGMa5UPtDb8Lfgl/f/ugmUjlV8TZ6n6lacQPXu/B7FtJ1iTKS7nhc5EGmMXtCI/SvbrgRuMS2gASWy1WvcV7DE6E4KrDs/qQImrjPTV1S27H4ZWa2MAA1aFF3uudoSYVN8DbSuTJolqlTlSBuvpcJMoyRz77Fyy8LFgNOeBonRE56Km78B84qjorT937SZ9Vp3P3GSETmUylWQNFWdvgfJP5Hdlw1LG6pBWxvxVEdsJuqFMWwY+cJ/blql0Vom0VQXGcdOEDl2hR4f+WGBjfpcK29YLJn1FNZCnhxHH0TCtBuZMxbOODZ0wtKnb2iqoKg==

On Wed, Jul 15, 2020 at 1:45 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

Another approach would be to ask the owner of the C code whether they have any objection to your publishing the proof. Seems to me your proving it would make their code more valuable.

The C code is available publically under GPLv2 license. The main question is whether the correctness proof (just the .v file(s) containing the specs and proofs, NOT the code or the .v file containing the code AST) can be released under a different license (possibly incompatible with GPLv2).

[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
        
        Re: [Coq-Club] license: derivative status of proofs, Stefan Monnier, 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
        Re: [Coq-Club] license: derivative status of proofs, Xuanrui Qi, 07/16/2020
        Re: [Coq-Club] license: derivative status of proofs, Kevin Sullivan, 07/16/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Gabriel Scherer, 07/17/2020
      - Re: [Coq-Club] license: derivative status of proofs, Maximilian Wuttke, 07/15/2020
        
        Re: [Coq-Club] license: derivative status of proofs, Kevin Sullivan, 07/15/2020