coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] license: derivative status of proofs
Date: Tue, 14 Jul 2020 23:38:47 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f182.google.com
Ironport-phdr: 9a23:JXal4h9PzH1Rqf9uRHKM819IXTAuvvDOBiVQ1KB42uocTK2v8tzYMVDF4r011RmVBNudsKsP2rWempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgRFiCCzbL9vIxm7qQfcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh/27XhM5/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZOehYroz9rEYOoxSgBQmsHufvxSFVjXLx36060uEhHRvI3AM+H9IOqnDUo8vuOacdVOC61qjIzTHZY/xK3jf97ZHFfxY8qv6DQbx+a9DeyVUzFwzblFWQr5ToMi+W2+kTt2WW4OttWOathmI7tQx/rDyiytswh4TNmo4Yy17J+CRnzYsrOdG1TEp2bNyrHZVeqiyUOJZ7T90+T2xupS00yaUGtIalcCQWzJkr3R3SZvydf4SV4x/uVfydLSp7iX57fr+0mgy8/lK6yuLmU8m5yFZKoTRBktnLrn0N0gbc6smDSvdk/0eh3SuD2xnd6u1ZIk04i7DXK5Emwr43mZoTtVrMEjXql0Xxia+abkQk+u625OT7erjquIOQOotuhgz9MqkigNGzDOU5PwQUQmSW+vqw2KXm/ULjQbVKivM2krPesJDfPckbpK+5AwpP3oYt9Rm/Dy2m0NAGknQcI1JFfQiIj4ntO13UPP/4CvK/j0y2kDh33/DGIqHhApLVI3ffl7fhZK9x5FJYyAou1t9S/IlUC7EEIPLrQED9rt3YDhkjMwy12enrEtt91plNEV6IV6SeKebZtUKCzuMpOeiFIoEP6xjnLP1wxf/rxVE0mUUZcOH935oSLn61Hu5iLm2WZHPthpEKFmJc7Vl2d/DjlFDXCW0bXH21Ra9pvmhqWrLjNp/KQ8WWuJLE2S66GpNMYWUfUwKDFH7pc8OPXPJeMXvOcP8kqSQNUP2ac6FkzQun7VaoxL9uL+6S8Sod58q6iYpFotbLnBR3zgRaSsSQ12bXETNxl2IMAj4yheVx+BwnjFiE1qd8jrpTEtkBv/4=

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