{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:53:34Z","timestamp":1776891214151,"version":"3.51.2"},"reference-count":65,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T00:00:00Z","timestamp":1736294400000},"content-version":"unspecified","delay-in-days":7,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes monadic equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws as interfaces like it is done when formalizing hierarchy of algebras in dependent-type theory. Thanks to this approach, we clearly separate equational laws from models. We can then take advantage of the sophisticated rewriting capabilities of Coq and build libraries of lemmas to achieve concise proofs of programs. We can also use the resulting framework to leverage on Coq\u2019s mathematical theories and formalize models of monads. In this article, we explain how we formalize a rich hierarchy of effects (nondeterminism, state, probability, etc.), how we mechanize examples of monadic equational reasoning from the literature, and how we apply our framework to the design of equational laws for a subset of ML with references.<\/jats:p>","DOI":"10.1017\/s0956796824000157","type":"journal-article","created":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T04:06:31Z","timestamp":1736309191000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["A practical formalization of monadic equational reasoning in dependent-type theory"],"prefix":"10.46298","volume":"35","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":"25203","published-online":{"date-parts":[[2025,1,8]]},"reference":[{"key":"S0956796824000157_ref25","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. Springer, pp. 23\u201367.","DOI":"10.1007\/978-3-642-35705-3_2"},{"key":"S0956796824000157_ref51","unstructured":"Mu, S. (2019a) Calculating a Backtracking Algorithm: An Exercise in Monadic Program Derivation. Technical Report TR-IIS-19-003. Academia Sinica."},{"key":"S0956796824000157_ref46","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796824000157_ref6","unstructured":"Affeldt, R. , Garrigue, J. & Saikawa, T. (2023) Environment-friendly monadic equational reasoning for OCaml. In The Coq Workshop 2023, Bia\u0142ystok, Poland, July 31, 2023. Abstract available at: https:\/\/coq-workshop.gitlab.io\/2023\/abstracts\/coq2023_monadic-reasoning.pdf."},{"key":"S0956796824000157_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364532"},{"key":"S0956796824000157_ref2","unstructured":"Abou-Saleh, F. , Cheung, K.-H. & Gibbons, J. (2016) Reasoning about probability and nondeterminism. In POPL Workshop on Probabilistic Programming Semantics."},{"key":"S0956796824000157_ref48","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796824000157_ref20","unstructured":"CoqGen. (2021) A Coq generation backend for OCaml. Available at: https:\/\/github.com\/COCTI\/ocaml\/pull\/3. Authors: Jacques Garrigue, Takafumi Saikawa et al. Last modification: 2024."},{"key":"S0956796824000157_ref47","unstructured":"MathComp. (2024) The mathematical components repository. Available at: https:\/\/github.com\/math-comp\/math-comp. Version 2.2.0."},{"key":"S0956796824000157_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_1"},{"key":"S0956796824000157_ref1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.12232"},{"key":"S0956796824000157_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16912-0_6"},{"key":"S0956796824000157_ref30","unstructured":"Infotheo. (2018) Infotheo: A Coq formalization of information theory and linear error-correcting codes. Available at: https:\/\/github.com\/affeldt-aist\/infotheo. Authors: Reynald Affeldt, Manabu Hagiwara, Jonas S\u00e9nizergues, Jacques Garrigue, Kazuhiko Sakaguchi, Taku Asai, Takafumi Saikawa, and Naruomi Obata. Last stable release: 0.7.4 (2024)."},{"key":"S0956796824000157_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.06.012"},{"key":"S0956796824000157_ref62","unstructured":"Sterling, J. , Gratzer, D. & Birkedal, L. (2022) Denotational semantics of general store and polymorphism. CoRR. abs\/2210.02169."},{"key":"S0956796824000157_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"S0956796824000157_ref3","unstructured":"Aczel, P. (1977) The strength of Martin-L\u00f6f\u2019s intuitionistic type theory with one universe. In Symposiums on mathematical logic in Oulu 1974 and in Helsinki 1975, 1\u201332."},{"key":"S0956796824000157_ref31","first-page":"1","volume-title":"IFIP TCS","author":"Jacobs","year":"2010"},{"key":"S0956796824000157_ref65","unstructured":"Voevodsky, V. , Ahrens, B. , Grayson, D. et al. (2014) UniMath\u2014a computer-checked library of univalent mathematics. Available at: https:\/\/github.com\/UniMath\/UniMath."},{"key":"S0956796824000157_ref28","unstructured":"Builder, Hierarchy . (2021) Hierarchy builder wiki\u2014missingjoin. Available at: https:\/\/github.com\/math-comp\/hierarchy-builder\/wiki\/MissingJoin."},{"key":"S0956796824000157_ref11","unstructured":"Benton, N. , Hughes, J. & Moggi, E. (2000) Monads and effects. In Applied Semantics, International Summer School (APPSEM 2000), Caminha, Portugal, September 9\u201315, 2000, Advanced Lectures. Springer, pp. 42\u2013122."},{"key":"S0956796824000157_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_9"},{"key":"S0956796824000157_ref18","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.102.15"},{"key":"S0956796824000157_ref27","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","journal-title":"J. Formaliz. Reasoning"},{"key":"S0956796824000157_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000137"},{"key":"S0956796824000157_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"S0956796824000157_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"S0956796824000157_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"S0956796824000157_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"S0956796824000157_ref60","doi-asserted-by":"crossref","unstructured":"Spector-Zabusky, A. , Breitner, J. , Rizkallah, C. & Weirich, S. (2018) Total Haskell is reasonable Coq. In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, CA, USA, January 8\u20139, 2018. ACM, pp. 14\u201327.","DOI":"10.1145\/3176245.3167092"},{"key":"S0956796824000157_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_16"},{"key":"S0956796824000157_ref33","unstructured":"Jaskelioff, M. (2009b) Lifting of Operations in Modular Monadic Semantics. PhD thesis. University of Nottingham. Available at: https:\/\/www.fceia.unr.edu.ar\/mauro\/pubs\/Thesis.pdf."},{"key":"S0956796824000157_ref63","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"S0956796824000157_ref64","volume-title":"The Coq Proof Assistant Reference Manual","year":"2024"},{"key":"S0956796824000157_ref24","unstructured":"Garrigue, J. & Saikawa, T. (2022) Validating OCaml soundness by translation into Coq. In 28th International Conference on Types for Proofs and Programs (TYPES 2022), Nantes, France, 20\u201325 June, 2022. Abstract available at: https:\/\/www.math.nagoya-u.ac.jp\/~garrigue\/papers\/types2022.pdf. Implementation: A Coq generation backend for OCaml. Available at: https:\/\/github.com\/COCTI\/ocaml\/pull\/3. Authors: Jacques Garrigue, Takafumi Saikawa et al. Last modification: 2024."},{"key":"S0956796824000157_ref43","unstructured":"Maillard, K. (2019) Principes de la V\u00e9rification de Programmes \u00e0 Effets Monadiques Arbitraires. PhD thesis. Universit\u00e9 PSL."},{"key":"S0956796824000157_ref50","unstructured":"Mu, S. (2019) Equational Reasoning for Non-determinism Monad: A Case Study of Spark Aggregation. Technical Report TR-IIS-19-002. Academia Sinica."},{"key":"S0956796824000157_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796822000120"},{"key":"S0956796824000157_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"S0956796824000157_ref15","unstructured":"Cheung, K.-H. (2017) Distributive Interaction of Algebraic Effects. PhD thesis. Merton College, University of Oxford."},{"key":"S0956796824000157_ref44","first-page":"1","article-title":"Dijkstra monads for all","volume":"3","author":"Maillard","year":"2019","journal-title":"PACMPL"},{"key":"S0956796824000157_ref19","unstructured":"Cohen, C. , Sakaguchi, K. & Tassi, E. (2020) Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), June 29\u2013July 6, 2020, Paris, France (Virtual Conference). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp. 34:1\u201334:21."},{"key":"S0956796824000157_ref49","unstructured":"Monae. (2018) Monae: Monadic effects and equational reasonig in Coq. Available at: https:\/\/github.com\/affeldt-aist\/monae. Authors: Reynald Affeldt, David Nowak, Takafumi Saikawa, Jacques Garrigue, Ayumu Saito, Celestine Sauvage, and Kazunari Tanaka. Last stable release: 0.7.1 (2024)."},{"key":"S0956796824000157_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_20"},{"key":"S0956796824000157_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_8"},{"key":"S0956796824000157_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342592"},{"key":"S0956796824000157_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_5"},{"key":"S0956796824000157_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59647-1_31"},{"key":"S0956796824000157_ref57","unstructured":"Shan, C.-C. (2018) Equational reasoning for probabilistic programming. In POPL 2018 TutorialFest."},{"key":"S0956796824000157_ref36","unstructured":"Jones, M. P. & Duponcheel, L. (1993) Composing monads. Technical Report YALEU\/DCS\/RR-1004. Yale University."},{"key":"S0956796824000157_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"S0956796824000157_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1524-5_1"},{"key":"S0956796824000157_ref12","volume-title":"Series","author":"Bertot","year":"2004"},{"key":"S0956796824000157_ref7","unstructured":"Affeldt, R. & Nowak, D. (2020) Extending equational monadic reasoning with monad transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020), March 2\u20135, 2020, University of Turin, Italy. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp. 2:1\u20132:21."},{"key":"S0956796824000157_ref17","unstructured":"Claret, G. (2018) Program in Coq. (Programmer en Coq). PhD thesis. Paris Diderot University, France."},{"key":"S0956796824000157_ref56","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102372"},{"key":"S0956796824000157_ref37","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005109"},{"key":"S0956796824000157_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.011"},{"key":"S0956796824000157_ref42","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3999478"},{"key":"S0956796824000157_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_2"},{"key":"S0956796824000157_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"S0956796824000157_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_6"},{"key":"S0956796824000157_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000354"},{"key":"S0956796824000157_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"S0956796824000157_ref45","unstructured":"Martin-Dorel, E. & Tassi, E. (2019) SSReflect in Coq 8.10. In The Coq Workshop 2019, Portland State University, Portland, OR, USA, September 8, 2019. Presentation slides available at: https:\/\/staff.aist.go.jp\/reynald.affeldt\/coq2019\/coqws2019-martindorel-tassi-slides.pdf."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796824000157","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:17:56Z","timestamp":1776889076000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796824000157\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":65,"alternative-id":["S0956796824000157"],"URL":"https:\/\/doi.org\/10.1017\/s0956796824000157","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e1"}}