{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:15:51Z","timestamp":1742991351541,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030535179"},{"type":"electronic","value":"9783030535186"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_2","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"23-38","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Adventures in Convex and Conical Spaces"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2327-953X","authenticated-orcid":false,"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8056-5519","authenticated-orcid":false,"given":"Jacques","family":"Garrigue","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4492-745X","authenticated-orcid":false,"given":"Takafumi","family":"Saikawa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"issue":"1","key":"2_CR1","first-page":"43","volume":"11","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11(1), 43\u201376 (2018)","journal-title":"J. Formaliz. Reason."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Garrigue, J., Nowak, D., Saikawa, T.: A trustful monad for axiomatic reasoning with probability and nondeterminism, March 2020, https:\/\/arxiv.org\/abs\/2003.09993","DOI":"10.1017\/S0956796821000137"},{"key":"2_CR3","unstructured":"Affeldt, R., et al.: Monadic equational reasoning in Coq (2019). https:\/\/github.com\/affeldt-aist\/monae\/, Coq scripts"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Examples of formal proofs about data compression. In: International Symposium on Information Theory and Its Applications (ISITA 2018), Singapore, 28\u201331 October 2018, pp. 665\u2013669. IEICE, IEEE Xplore, October 2018","DOI":"10.23919\/ISITA.2018.8664276"},{"key":"2_CR5","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Reasoning with conditional probabilities and joint distributions in Coq. Computer Software (2020, to appear). Japan Society for Software Science and Technology. https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/cproba_preprint.pdf"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10817-013-9298-1","volume":"53","author":"R Affeldt","year":"2014","unstructured":"Affeldt, R., Hagiwara, M., S\u00e9nizergues, J.: Formalization of Shannon\u2019s theorems. J. Autom. Reason. 53(1), 63\u2013103 (2014)","journal-title":"J. Autom. Reason."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-030-33636-3_9","volume-title":"Mathematics of Program Construction","author":"R Affeldt","year":"2019","unstructured":"Affeldt, R., Nowak, D., Saikawa, T.: A hierarchy of monadic effects for program verification using equational reasoning. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 226\u2013254. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-33636-3_9"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Beaulieu, G.: Probabilistic completion of nondeterministic models. Ph.D. thesis, University of Ottawa (2008)","DOI":"10.1016\/j.entcs.2007.02.028"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86\u2013101. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_11"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 85, pp. 23:1\u201323:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.23","DOI":"10.4230\/LIPIcs.CONCUR.2017.23"},{"key":"2_CR11","unstructured":"Cheung, K.H.: Distributive interaction of algebraic effects. Ph.D. thesis, University of Oxford (2017)"},{"key":"2_CR12","volume-title":"Elements of Information Theory","author":"TM Cover","year":"2006","unstructured":"Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. Wiley, Hoboken (2006)","edition":"2"},{"issue":"4","key":"2_CR13","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1017\/S1446788700017973","volume":"30","author":"J Flood","year":"1981","unstructured":"Flood, J.: Semiconvex geometry. J. Aust. Math. Soc. 30(4), 496\u2013510 (1981). https:\/\/doi.org\/10.1017\/S1446788700017973","journal-title":"J. Aust. Math. Soc."},{"key":"2_CR14","unstructured":"Fritz, T.: Convex spaces I: Definition and examples (2015). https:\/\/arxiv.org\/abs\/0903.5522, First version: 2009"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-030-02508-3_25","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2018","author":"G van Heerdt","year":"2018","unstructured":"van Heerdt, G., Hsu, J., Ouaknine, J., Silva, A.: Convex language semantics for nondeterministic\u00a0probabilistic automata. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 472\u2013492. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_25"},{"key":"2_CR17","unstructured":"Infotheo: A Coq formalization of information theory and linear error-correcting codes (2020). https:\/\/github.com\/affeldt-aist\/infotheo\/, Coq scripts"},{"key":"2_CR18","unstructured":"Infotheo: probability\/convex_choice.v. In: [17] (2020), Coq scripts"},{"key":"2_CR19","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-15240-5_1","volume-title":"Theoretical Computer Science","author":"B Jacobs","year":"2010","unstructured":"Jacobs, B.: Convexity, duality and effects. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 1\u201319. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15240-5_1"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp. 186\u2013195, June 1989. https:\/\/doi.org\/10.1109\/LICS.1989.39173","DOI":"10.1109\/LICS.1989.39173"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Keimel, K., Plotkin, G.: Mixed powerdomains for probability and nondeterminism. Log. Meth. Comput. Sci. 13, December 2016. https:\/\/doi.org\/10.23638\/LMCS-13(1:2)2017","DOI":"10.23638\/LMCS-13(1:2)2017"},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1017\/S0960129509007555","volume":"19","author":"K Keimel","year":"2009","unstructured":"Keimel, K., Plotkin, G.D.: Predicate transformers for extended probability and non-determinism. Math. Struct. Comput. Sci. 19(3), 501\u2013539 (2009). https:\/\/doi.org\/10.1017\/S0960129509007555","journal-title":"Math. Struct. Comput. Sci."},{"key":"2_CR23","unstructured":"Kirch, O.: Bereiche und Bewertungen. Master\u2019s thesis, Technischen Hochschule Darmstadt (1993)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-39634-2_5","volume-title":"Interactive Theorem Proving","author":"A Mahboubi","year":"2013","unstructured":"Mahboubi, A., Tassi, E.: Canonical structures for the working coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19\u201334. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_5"},{"key":"2_CR25","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01220869","volume":"21","author":"WD Neumann","year":"1970","unstructured":"Neumann, W.D.: On the quasivariety of convex subsets of affine spaces. Archiv der Mathematik 21, 11\u201316 (1970)","journal-title":"Archiv der Mathematik"},{"key":"2_CR26","unstructured":"Semadini, Z.: Banach Spaces of Continuous Functions. PWN (1971)"},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF02413910","volume":"29","author":"MH Stone","year":"1949","unstructured":"Stone, M.H.: Postulates for the barycentric calculus. Ann. Mat. Pura Appl. 29(1), 25\u201330 (1949)","journal-title":"Ann. Mat. Pura Appl."},{"key":"2_CR28","unstructured":"\u015awirszcz, T.: Monadic functors and convexity. Bulletin de l\u2019Acad\u00e9mie polonaise des sciences. S\u00e9rie des sciences math\u00e9matiques, astronomiques et physiques 22(1) (1974)"},{"key":"2_CR29","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2019). https:\/\/coq.inria.fr. Version 8.11.0"},{"key":"2_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.01.002","volume":"222","author":"R Tix","year":"2009","unstructured":"Tix, R., Keimel, K., Plotkin, G.: Semantic domains for combining probability and non-determinism. Electron. Notes Theor. Comput. Sci. 222, 3\u201399 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.01.002","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"2_CR31","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1017\/S0960129505005074","volume":"16","author":"D Varacca","year":"2006","unstructured":"Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87\u2013113 (2006)","journal-title":"Math. Struct. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T04:28:32Z","timestamp":1667449712000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}