coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Wed, 15 Jul 2020 22:03:39 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f171.google.com
Ironport-phdr: 9a23:mmikBxadaRUllk/RtOuypCz/LSx+4OfEezUN459isYplN5qZrsq9bnLW6fgltlLVR4KTs6sC17OI9fu7EjFaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsowjcuMYajIt8Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKxVrhK/qRJiwIDbYo+VOv1xcazBct0XXnZBU8RLWiBdGI6wc5UDAuwcNuhYtYn9oF4OoAOwCQmuA+PvzD5Ihnzo0q0+zesuDxrL3AMlH90UsXTUqM/5O7sVUeCwwqXD0DLOb/FR2Tf76YjIcQ4uofWSUr1uasfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri44IxV3J8Tt0zZs1KNO3RkB2YdGpHIVRuiyUOYV7RsMsTmNqtSs0xbMLuoK3cSkXxJg52hLSd/KKfpaH7B/tVOicJypzinxieLK6nRmy8E6gx/XgWcmzyFZLri5FncfCtnARzRDT7dKHSvR780y82jiPzxje5v9YLU0wj6bWKJ4szqQtmpcSrUjPBDL6lUfrgKOOaEkp+/Sk5/nib7n7opKTK4p5hw7/P6gyhsCyBPo0PRMAX2iV/Omx17Lu8lH3QLhPgP02nKzUsJ7EKssGpaO0BhNa3poj5hu/CTqtzc4WkmMdLF1ffRKKl4jpNE/KIPD/Ffq/hk6jkDZvx/zfJ73hHojBImHNkLv8f7tx9lRQyAU0zdBY6JJUDq8OLOjvVU/2sdzUFh45MwqqzOb7ENhxyJ8SVGaVDqKaMK7eq0KE6+MzL+WWeYMYuivxJ+Ag5/H0jH85nVEdfbOu3ZsScH24HPNmI0OYYXrvnNgBFXkFsRQlQezljV2NSz9TZ3KoU60g4TE7DZqqDZ3fSYC1nLyBwCC7E4VKaWBBE1CACGvnd4GZW/gXcy+SOc9gkjkcVbe7UYMh1BeutBX7y7V9NObU9DcY5trf041c7e3SjhE/9nRdCc2b3ynZRmt0n3gISjxw1aZ2p0A7y1af3oB3hvVZEZpY4PYfASkgMpuJhe59DdHxVwbMc/+GTV+nRpOtBjR7BoYzxNkPYEt5FtiKgRXK3i7sCLgQwe/YTKco+77RiiCib/12zGzLgfF40gsWB/BXPGjjvZZRsgjeA4mTzRecnqeuML0AhWvDrTjai2WJu05cXUh7VqCXBSlONHuTlszw4wb5d5HrDL0mNgVbzsvbc/lFb9ToiRNNQ/KxYY2CMVL0oH+5AFOz/p3JdJDjIjxP0yDUCUxCmAcWry6L

On Wed, 15 Jul 2020 18:36:51 -0700
Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> 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).

Found this, which may be relevant:
https://copyleft.org/guide/comprehensive-gpl-guidech5.html

Re: [Coq-Club] license: derivative status of proofs, (continued)
- 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
- Re: [Coq-Club] license: derivative status of proofs, Xuanrui Qi, 07/15/2020