{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:56Z","timestamp":1776891476825,"version":"3.51.2"},"reference-count":51,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"unspecified","delay-in-days":195,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a nontrivial interface, which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.<\/jats:p>","DOI":"10.1017\/s0956796821000137","type":"journal-article","created":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:22:51Z","timestamp":1626308571000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":11,"title":["A trustful monad for axiomatic reasoning with probability and nondeterminism"],"prefix":"10.46298","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2327-953X","authenticated-orcid":false,"given":"REYNALD","family":"AFFELDT","sequence":"first","affiliation":[]},{"given":"JACQUES","family":"GARRIGUE","sequence":"additional","affiliation":[]},{"given":"DAVID","family":"NOWAK","sequence":"additional","affiliation":[]},{"given":"TAKAFUMI","family":"SAIKAWA","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"S0956796821000137_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_18"},{"key":"S0956796821000137_ref39","unstructured":"Monae. (2021) Monadic Effects and Equational Reasoning in Coq. https:\/\/github.com\/affeldt-aist\/monae. Open source software. Since 2018. Version 0.3.2. Software Heritage Archive: swh:1:dir:2d68878d365fe72744f8b085fa29df385567f6c9."},{"key":"S0956796821000137_ref49","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"S0956796821000137_ref19","unstructured":"Fritz, T. (2015) Convex Spaces I: Definition and Examples. https:\/\/arxiv.org\/abs\/0903.5522. arXiv math.MG. First version: 2009."},{"key":"S0956796821000137_ref13","unstructured":"Bonchi, F. , Sokolova, A. & Vignudelli, V. (2020b) The Theory of Traces for Systems with Nondeterminism, Probability, and Termination. https:\/\/arxiv.org\/abs\/1808.00923v4. arXiv cs.LO."},{"key":"S0956796821000137_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_5"},{"key":"S0956796821000137_ref35","doi-asserted-by":"crossref","unstructured":"McIver, A. & Morgan, C. (2005) Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer.","DOI":"10.1145\/1059816.1059824"},{"key":"S0956796821000137_ref50","unstructured":"Voevodsky, V. , Ahrens, B. , Grayson, D. , et al. (2014) UniMath \u2014 A Computer-Checked Library of Univalent Mathematics. Available at: https:\/\/github.com\/UniMath\/UniMath. Last stable release 0.1 (2016)."},{"key":"S0956796821000137_ref51","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785707"},{"key":"S0956796821000137_ref33","unstructured":"Mathematical Components Team. (2007) Mathematical Components Library. https:\/\/github.com\/math-comp\/math-comp. Development version. Last stable version 1.12 (2020). Available on the same website."},{"key":"S0956796821000137_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034777"},{"key":"S0956796821000137_ref34","unstructured":"McBride, C. (1999) Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh."},{"key":"S0956796821000137_ref18","unstructured":"Cohen, C. , Sakaguchi, K. & Tassi, E. (2020) Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In FSCD 2020. LIPIcs, vol. 167, pp. 34:1\u201334:21."},{"key":"S0956796821000137_ref6","first-page":"79","article-title":"Reasoning with conditional probabilities and joint distributions in Coq","volume":"37","author":"Affeldt","year":"2020","journal-title":"Comput. Softw."},{"key":"S0956796821000137_ref41","unstructured":"Mu, S.-C. (2019b) Equational Reasoning for Non-deterministic Monad: A Case study of Spark Aggregation. Tech. rept. TR-IIS-19-002. Institute of Information Science, Academia Sinica."},{"key":"S0956796821000137_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9298-1"},{"key":"S0956796821000137_ref12","unstructured":"Bonchi, F. , Sokolova, A. & Vignudelli, V. (2020a) Presenting convex sets of probability distributions by convex semilattices and unique bases. https:\/\/arxiv.org\/abs\/2005.01670. arXiv cs.LO."},{"key":"S0956796821000137_ref15","unstructured":"Cheung, K.-H. (2017) Distributive Interaction of Algebraic Effects. PhD thesis, Merton College, University of Oxford."},{"key":"S0956796821000137_ref26","unstructured":"Infotheo. (2021) A Coq Formalization of Information Theory and Linear Error-Correcting Codes. https:\/\/github.com\/affeldt-aist\/infotheo. Open source software. Since 2009. Version 0.3.2. Software Heritage Archive: swh:1:dir:f8c270f648dd5bc6f822ef16e9354195ddb8f6ad."},{"key":"S0956796821000137_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0083084"},{"key":"S0956796821000137_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"S0956796821000137_ref45","unstructured":"The Coq Development Team. (2019) The Logic of Coq. Available at: https:\/\/github.com\/coq\/coq\/wiki\/The-Logic-of-Coq. Part of the Coq FAQ."},{"key":"S0956796821000137_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-0208(08)71950-9"},{"key":"S0956796821000137_ref47","unstructured":"Timany, A. & Jacobs, B. (2016) Category theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), June 22\u201326, 2016, Porto, Portugal, Kesner, D. and Pientka, B. (eds), LIPIcs, vol. 52, pp. 30:1\u201330:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik."},{"key":"S0956796821000137_ref16","unstructured":"Cock, D. (2014) Leakage in Trustworthy Systems. PhD thesis, School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia."},{"key":"S0956796821000137_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"S0956796821000137_ref3","first-page":"43","article-title":"Formalization techniques for asymptotic reasoning in classical analysis","volume":"11","author":"Affeldt","year":"2018","journal-title":"J. Formaliz. Reason."},{"key":"S0956796821000137_ref11","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785673"},{"key":"S0956796821000137_ref17","unstructured":"Cohen, C. & Sakaguchi, K. (2015) A Finset and Finmap Library: Finite Sets, Finite Maps, Multisets and Order. Available at: https:\/\/github.com\/math-comp\/finmap. Last stable release: 1.5.0 (2020)."},{"key":"S0956796821000137_ref46","volume-title":"The Coq Proof Assistant Reference Manual","year":"2021"},{"key":"S0956796821000137_ref36","unstructured":"Mio, M. & Vignudelli, V. (2020) Monads and Quantitative Equational Theories for Nondeterminism and Probability. https:\/\/arxiv.org\/abs\/2005.07509. arXiv cs.LO."},{"key":"S0956796821000137_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_1"},{"key":"S0956796821000137_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"S0956796821000137_ref31","unstructured":"Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics, vol. 5. Berlin and New York: Springer-Verlag."},{"key":"S0956796821000137_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"S0956796821000137_ref10","unstructured":"Bonchi, F. , Silva, A. & Sokolova, A. (2017) The power of convex algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017), September 5\u20138, 2017, Berlin, Germany, Meyer, R. & Nestmann, U. (eds), LIPIcs, vol. 85. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp. 23:1\u201323:18."},{"key":"S0956796821000137_ref29","first-page":"1","article-title":"Mixed powerdomains for probability and nondeterminism","volume":"13","author":"Keimel","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S0956796821000137_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_26"},{"key":"S0956796821000137_ref40","unstructured":"Mu, S.-C. (2019a) Calculating a Backtracking Algorithm: An Exercise in Monadic Program Derivation. Tech. rept. TR-IIS-19-003. Institute of Information Science, Academia Sinica."},{"key":"S0956796821000137_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_9"},{"key":"S0956796821000137_ref21","doi-asserted-by":"crossref","unstructured":"Gibbons, J. (2012) Unifying theories of programming with monads. In Revised Selected Papers of the 4th International Symposium on Unifying Theories of Programming (UTP 2012), Paris, France, August 27\u201328, 2012, Wolff, B. , Gaudel, M. and Feliachi, A. (eds), Lecture Notes in Computer Science, vol. 7681. Springer, pp. 23\u201367.","DOI":"10.1007\/978-3-642-35705-3_2"},{"key":"S0956796821000137_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S0956796821000137_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11478-1"},{"key":"S0956796821000137_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394795"},{"key":"S0956796821000137_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BF02413910"},{"key":"S0956796821000137_ref44","unstructured":"The Agda Team. (2020) The Agda User Manual. Available at: https:\/\/agda.readthedocs.io\/en\/v2.6.0.1. Version 2.6.0.1."},{"key":"S0956796821000137_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"S0956796821000137_ref5","doi-asserted-by":"crossref","unstructured":"Affeldt, R. , Garrigue, J. & Saikawa, T. (2020a) Formal adventures in convex and conical spaces. In 13th International Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Italy, July 26\u201331, 2020, Benzm\u00fcller, C. & Miller, B. R. (eds), Lecture Notes in Computer Science, vol. 12236. Springer, pp. 23\u201338.","DOI":"10.1007\/978-3-030-53518-6_2"},{"key":"S0956796821000137_ref7","unstructured":"Beaulieu, G. (2008) Probabilistic Completion of Nondeterministic Models. PhD thesis, Faculty of Graduate and Postdoctoral Studies, University of Ottawa."},{"key":"S0956796821000137_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.04.019"},{"key":"S0956796821000137_ref1","unstructured":"Abou-Saleh, F. , Cheung, K.-H. & Gibbons, J. (2016) Reasoning about probability and nondeterminism. In POPL Workshop on Probabilistic Programming Semantics."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796821000137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:20:12Z","timestamp":1776889212000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796821000137\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":51,"alternative-id":["S0956796821000137"],"URL":"https:\/\/doi.org\/10.1017\/s0956796821000137","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e17"}}