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: Wed, 15 Jul 2020 06:46:33 -0400
Authentication-results: mail2-smtp-roc.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-ej1-f43.google.com
Ironport-phdr: 9a23:neqZEBboxMnZ4zk9MS9sqj//LSx+4OfEezUN459isYplN5qZr867bnLW6fgltlLVR4KTs6sC17OI9fu6Ejdcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsowjdqMYajIVtJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1UoByjqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xaZYEAeobPeZfqonwv14AogWgBQmtAuPk1yJGhmLy3a0+0uQhDxvJ3Ao9FN8Jq3TUsdH1NKMTUeCr1qbIyy/Pb/BI1jfj6YjIdBIhrOqDXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkCvGaH9eRvT/6vi3I5pAFrpDii3tohhpTUio8RxF7J+ip3zYQ1K9GlSkN2YtqpHIZQuSyHKYZ6XswvTW90tCskxbALtp22cSkUxZg5yRPSa/+KfomO7xn+V+iROS91iGx5dL+7nRq/8kitxvfiWsWp01tGtCVIn9fKu3sQzRLc8NKHReF4/kq52TaAyQTT6uZcLEAxj6XbKpohzqcumZoRrEjPByH2lUr4gaOMeUUk/e+o6+vjYrr4vJOTK4h0igTmPqQvnMywH/g4PxAQU2SH/emwzr7u8E3jTLlUk/E7kbPVvZ/UKMgDo662GQ5V0oIt6xalCDem1cwVnWIaLFJBfBKHjpbpNEvIIPziDvewnUqskDZtx/DEJbDhDZDNIWLCkLflZ7py90lcyA8rwdBF+51UEq0BIO70WkLpqNPYCQY5PxWozObjFdVyzZgTWXmPA6+cKKPdq0WE5uMpI+mWZY8aoizxK/Y/562msXhsklgEOKKtwJE/aXaiH/0gLV/KT2Drh4IiHHkLuEIFUejuiUOLV3YHfGu2W6Mi7zd9C4+4DIHBbo+oib2Fmiy8G8sFNSh9FlmQHCKwJM2/UPAWZXfKe5Izonk/TbGkDrQZ+1SuuQv9kec1K+PV/mgVt8um2oQuoeLUkh42+Hp/CMHPizjRHVExpXsBQnoN5I46uVZ0kw7R3q1xgvgeHttWtasQA1UKcKXExuk/MOjcHwfIf9OHUlGjG4z0DjQ4T9Z3yNgLMR9w

Pretty interesting question. Thanks for raising it. --Kevin

On Wed, Jul 15, 2020 at 2:40 AM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

I have to agree with Xuanrui. If it's important, talk to an attorney. Maybe your institution has some IP experts who can help you. It may matter what country you're in unless you want an answer for all the major countries. Your exact question may be new for the lawyers.

Sounds like you got the C code under a license that prohibits or limits creating derivative works. There may be other important terms in the license to consider, too.

[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