Re: [isabelle-dev] isabelle-dev Digest, Vol 134, Issue 14
Dear David Blubaugh, It is interesting that, some days ago, I had a similar idea with respect to Kickstarter and Isabelle, but by motivation comes from medicine. My project was to write a paper and some thy files in order to decide if a given sample of adenosine triphosphate is generated by respiration (a normal cell) or by fermentation (a cancer cell). The thy files will be the reward for people donating 1000 Canadian dollars. There are several mathematical ways to study the structure of a molecule: moduli spaces, knots, fractals, etc. Even if this project may not attend his funding, it will be interesting at least as a social experiment. I hope that it will popularize a little bit Otto Warburg's theory about the origin of cancer cells, which is controversial, but it has not been refuted yet. You could read my projet here: https://www.kickstarter.com/projects/1176467506/cancer-vs-mathematics Sincerely yours, Jose M. Message: 1 > Date: Thu, 26 Jul 2018 07:13:22 + (UTC) > From: David Blubaugh > To: "isabelle-dev@mailbroy.informatik.tu-muenchen.de" > , > "isabelle-dev-requ...@mailbroy.informatik.tu-muenchen.de" > , > "isabelle-dev-ow...@mailbroy.informatik.tu-muenchen.de" > , > "isabelle-us...@cl.cam.ac.uk" > Subject: [isabelle-dev] Kickstarter Campaign based on Isabelle HOL > Technologies > Message-ID: <849313566.2576703.1532589202...@mail.yahoo.com> > Content-Type: text/plain; charset="utf-8" > > To All,?? > > I am currently a developer and user of Isabelle HOL technologies and I am > currently in the process of developing a Kickstarter campaign based on the > use of Isabelle HOL being used in the creation of a specific software > application for use within mobile devices.?? > > Would anyone be interested in knowing more on this potential Kickstarter > campaign ? > Thanks, > > David Blubaugh > Isabelle HOL user since 2008.? ? > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] a question about regulations
Hi Makarius and Gerwin, Thank you by the information. I sorry if this mailing list was not the best to ask this legal question, I did not find another one more appropriated for this subject. With respect to Makarius worries with open source, I'm the first who enjoys open source. Kind Regards, José M. 2018-06-28 12:06 GMT+02:00 Makarius : > On 28/06/18 07:55, José Manuel Rodriguez Caballero wrote: > > > > Motivated by my exchange of experiences with professionals using > > proof-assistants like Coq for commercial purposes, I would like to ask > > the following question is: which are the regulations of Isabelle for > > commercial use? For example, if a software company is interested in > > selling .thy files to clients, which conditions apply? > > (Why is this on isabelle-dev? It is not relevant to the Isabelle > development process. Isabelle theory development is a normal user > activity.) > > Isabelle itself is subject to the very liberal BSD-style license scheme. > Its add-on tools might have other Open Source licenses. The overall > Isabelle application taken together converges to the strictest Open > Source license of any of its components, similar to a Linux distribution. > > Whatever you produce yourself with the Isabelle application is *not* > affected by any of this. You can publish your own outcome by whatever > license you like, even a non-Open-Source license. > > > But note that after some decades of Open Source culture, almost > everything of relevance is published Open Source now. Even if you "sell" > sources, you can often tell the one who pays for it that it is vital to > publish the results under such a reusable license: this will allow other > people in the same situation to build on it and improve the body of > available material in the next round of the universal iteration process. > > Ideally it will all end up in the Archive of Formal Proofs eventually, > where it is maintained "automagically", i.e. updated to new Isabelle > versions as they emerge. This is a privilege of the participants in the > Open Source cartel. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] a question about regulations
Dear Sir or Madam, Motivated by my exchange of experiences with professionals using proof-assistants like Coq for commercial purposes, I would like to ask the following question is: which are the regulations of Isabelle for commercial use? For example, if a software company is interested in selling .thy files to clients, which conditions apply? Sincerely yours, José M.l Rodriguez Caballero Université du Québec à Montréal ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
