{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:35:53Z","timestamp":1761510953756},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22673-1_11","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T11:49:15Z","timestamp":1310557755000},"page":"149-163","source":"Crossref","is-referenced-by-count":14,"title":["Licensing the Mizar Mathematical Library"],"prefix":"10.1007","author":[{"given":"Jesse","family":"Alama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lionel","family":"Mamane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Rudnicki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","first-page":"579","volume-title":"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project AUTOMATH. In: Hindley, R., Seldin, J. (eds.) To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms, pp. 579\u2013606. Academic Press, London (1980)"},{"key":"11_CR2","unstructured":"Creative Commons BY-SA, \n                    \n                      http:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/\n                    \n                    \n                   (last accessed 2011\/03\/14)"},{"key":"11_CR3","unstructured":"Free Software Foundation Europe, Fiduciary License Agreement (FLA), \n                    \n                      http:\/\/fsfe.org\/projects\/ftf\/fla.en.html"},{"key":"11_CR4","unstructured":"The FLOSSmole project, \n                    \n                      http:\/\/flossmole.org\/"},{"key":"11_CR5","unstructured":"Free Software Foundation: The GNU General Public License, version 3 (June 29, 2007), \n                    \n                      http:\/\/www.gnu.org\/licenses\/gpl.html"},{"key":"11_CR6","unstructured":"Licenses \u2013 definitions of free cultural works. \n                    \n                      http:\/\/freedomdefined.org\/Licenses"},{"key":"11_CR7","unstructured":"Various licenses and comments about them, \n                    \n                      http:\/\/www.gnu.org\/licenses\/license-list.html"},{"key":"11_CR8","unstructured":"Hillesley, R.: Copyright assignment\u2013once bitten, twice shy. The H Open (August 6, 2010), \n                    \n                      http:\/\/www.h-online.com\/open\/features\/Copyright-assignment-Once-bitten-twice-shy-1049631.html"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"17","DOI":"10.4018\/jitwe.2006070102","volume":"1","author":"J. Howison","year":"2006","unstructured":"Howison, J., Conklin, M., Crowston, K.: FLOSSmole: A collaborative repository for FLOSS research data and analyses. International Journal of Information Technology and Web Engineering\u00a01, 17\u201326 (2006), current data \n                    \n                      http:\/\/flossmole.org\/content\/using-flossmole-data","journal-title":"International Journal of Information Technology and Web Engineering"},{"key":"11_CR10","unstructured":"Jackson, T., Dance, G., Ko, H., Kueneman, A., Bost, K., Meek, M.: IBM\u2019s Watson trivia challenge, \n                    \n                      http:\/\/www.nytimes.com\/interactive\/2010\/06\/16\/magazine\/watson-trivia-game.html"},{"key":"11_CR11","unstructured":"van Benthem, L.S.: Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH System, Mathematical Centre Tracts, vol.\u00a083. Mathematisch Centrum, Amsterdam, Netherlands (1979)"},{"key":"11_CR12","unstructured":"Kuhn, B.M.: Not all copyright assignment is created equal (February 1, 2010), \n                    \n                      http:\/\/ebb.org\/bkuhn\/blog\/2010\/02\/01\/copyright-not-all-equal.html"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11617990_11","volume-title":"Types for Proofs and Programs","author":"L.E. Mamane","year":"2006","unstructured":"Mamane, L.E.: Surreal numbers in coq. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 170\u2013185. Springer, Heidelberg (2006), doi:10.1007\/11617990_11"},{"key":"11_CR14","unstructured":"The Mizar Mathematical Library. Browsable online, \n                    \n                      http:\/\/mizar.org\/"},{"issue":"2","key":"11_CR15","first-page":"265","volume":"6","author":"A. Naumowicz","year":"1997","unstructured":"Naumowicz, A.: Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics\u00a06(2), 265\u2013268 (1997)","journal-title":"Formalized Mathematics"},{"key":"11_CR16","unstructured":"Software, B.D.: Open source resource center\u2013license data, \n                    \n                      http:\/\/www.blackducksoftware.com\/oss\/licenses\n                    \n                    \n                   (last accessed March 2011)"},{"key":"11_CR17","unstructured":"Stallman, R.M.: Free Software Free Society: Selected Essays, 1st edn. ch.15, p. 91. GNU Press (2002); 2nd edn, \n                    \n                      http:\/\/shop.fsf.org\/product\/free-software-free-society-2\/\n                    \n                    \n                  ; chapter 15: \n                    \n                      http:\/\/www.gnu.org\/philosophy\/pragmatic.html"},{"key":"11_CR18","unstructured":"Stallman, R.M.: When a company asks for your copyright (September 29, 2010), \n                    \n                      http:\/\/www.fsf.org\/blogs\/rms\/assigning-copyright"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-36469-2_16","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2003","unstructured":"Urban, J.: Translating Mizar for first order theorem provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 203\u2013215. Springer, Heidelberg (2003)"},{"issue":"1-2","key":"11_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. Journal of Automated Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR21","unstructured":"IBM Watson, \n                    \n                      http:\/\/www-03.ibm.com\/innovation\/us\/watson\/"},{"key":"11_CR22","unstructured":"Welte, H.: GPL enforcement. talk at FOSDEM 2005, (February 2005), abstract at \n                    \n                      http:\/\/archive.fosdem.org\/2005\/index\/speakers\/speakers_welte.html"},{"key":"11_CR23","unstructured":"Wheeler, D.A.: High assurance (for security or safety) and free-libre open source software (FLOSS)\u2026with lots on formal methods software verification, \n                    \n                      http:\/\/www.dwheeler.com\/essays\/high-assurance-floss.html\n                    \n                    \n                   (released 2006-06-02) (updated 2009-11-30)"},{"key":"11_CR24","unstructured":"Wheeler, D.A.: Make your open source software GPL-compatible. or else, \n                    \n                      http:\/\/www.dwheeler.com\/essays\/gpl-compatible.html\n                    \n                    \n                   (released 2002-05-06) (revised 2010-09-14)"},{"key":"11_CR25","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T01:59:07Z","timestamp":1553911147000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}