coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] license: derivative status of proofs
Date: Tue, 14 Jul 2020 17:38:27 -0700
Authentication-results: mail3-smtp-sop.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:apbD3xe0NcY8bZa4qWofNgxAlGMj4u6mDksu8pMizoh2WeGdxcSybB7h7PlgxGXEQZ/co6odzbaP7ea7ACdbvN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLRi6twvcutQZjYZsKqs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpUrxyhqRJxwJPabp+JO/dlZKzRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt5XwqEAOrRu/HgmsBP3gyjxVjXLq2601yeIhHhzb1wEnBd0Bq3TUrNTuNKcST++1z7PEwi/Fb/xM3zfy9ZLEchEgofGQUrJ9asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRmI8byk7J+Dh2zYg6ONC0VkB2bcCnHZZMuSyUN5V6T8wmTmxqpSo3yKALtJ67ciUIy5kqxQLTZ+KZf4WL4R/uWuCcKip2inJifbKwnRey8U64x+LgUcm0ylBKoTRBktnIrHwCyQHc6tWBR/Bg/UmhwS6C2x7P5uxAO0w5lqrWJ4Q8zrMxl5cfq0TOEjLwlU7rlqGZbF8k9fKt6+n/YrXpuJucN4hshwH7KKsum8i/Df05MggJQmSX4Oq82b3+8UHjT7VKifo2kqbdsJ/EP8gUuqm5AwpN3oYi7RawESum3cwGkXUbKF9JYhGKgojzN13TIf31DO2zjlSxnDtzwvDJJLzhApHDLnjZl7fheK5w5FRHxwozzNBf/JJUBa8CIP7pQEDxssbXDhkkPACuwubnCcl91owFVGKAB6+WKqLSsVuS6u0zJOmMYZcZuCzhJPg9+/7ukXg5lEcBcqmuxJsbcWy3HvB7I0qCenfsmdcAEWISvgUkVuDqiVuCUSRSZ3moRa486Cs7W8qaCtLIQZnoi7ic1m/vFZpPI2tCF1qkEHHydozCVe1aOwyIJco0uzYEVKOhRoxp/BensgOyn7NtLuvP+iAb85vl3d55oezSiR4a+jl9DsDb2GaIGTIn1lgUTiM7ifgs6Xd2zU2OhPAh3q5oUOdL7vYMaT8UcJ7Ry+sgVoL3UwPFO9aOEROoH4zgDjY2QdY8hdQJZhQlQoTwvlX4xyOvRoQtufmODZ0w/Ljb2iGodcl4wnfCkqImigt/G5cdBSidnqd6sjPrKcvRiUzAzvSlcK0d2GjG82LRlWc=

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/

[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