[isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)
makarius at sketis.net
Thu Jun 27 19:38:38 CEST 2013
On Wed, 26 Jun 2013, Stephen Nuchia wrote:
> Finally, I make my living in the commercial software world and I do not
> generally own the intellectual property I work on. I will often be less
> than completely open about the details of my work. I regret that but
> it's necessary.
Concerning anything that ends up in the Isabelle repository, it needs to
conform to the "ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER" of its
central COPYRIGHT file, with some potential add-on information in
CONTRIBUTORS and/or in individual file headers (at most one line as part
of "Author" info).
Intellectual property remains to whoever "owns" it, but by definition
these "owners" agree on the one Isabelle license. Thus you never need to
decide about ownership in practice -- the license takes precedence for all
relevant situations. This is a nice consequence of classical logic in a
Interestingly, the Coq guys -- being constructivists -- try to make this
decidable, by asking transfer of "IP ownership" of contributors, although
that is very hard to implement.
More information about the isabelle-dev