{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,29]],"date-time":"2025-12-29T22:14:57Z","timestamp":1767046497379,"version":"3.37.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030336356"},{"type":"electronic","value":"9783030336363"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-33636-3_9","type":"book-chapter","created":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:02:20Z","timestamp":1571479340000},"page":"226-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2327-953X","authenticated-orcid":false,"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"David","family":"Nowak","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":[[2019,10,20]]},"reference":[{"key":"9_CR1","unstructured":"Abou-Saleh, F., Cheung, K.H., Gibbons, J.: Reasoning about probability and nondeterminism. In: Workshop on Probabilistic Programming Semantics, St. Petersburg, FL, USA, 23 January 2016, January 2016"},{"issue":"1","key":"9_CR2","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":"9_CR3","unstructured":"Affeldt, R., Garrigue, J., Nowak, D., Saikawa, T.: A Coq formalization of monadic equational reasoning (2018). \n                    https:\/\/github.com\/affeldt-aist\/monae"},{"key":"9_CR4","unstructured":"Affeldt, R., et al.: A Coq formalization of information theory and linear error-correcting codes (2018). \n                    https:\/\/github.com\/affeldt-aist\/infotheo"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5\u201321. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-74591-4_3"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-319-59647-1_31","volume-title":"Networked Systems","author":"Y-F Chen","year":"2017","unstructured":"Chen, Y.-F., Hong, C.-D., Leng\u00e1l, O., Mu, S.-C., Sinha, N., Wang, B.-Y.: An executable sequential specification for spark aggregation. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 421\u2013438. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-59647-1_31"},{"key":"9_CR7","unstructured":"Cheung, K.H.: Distributive Interaction of Algebraic Effects. Ph.D. thesis, Merton College, University of Oxford (2017)"},{"key":"9_CR8","unstructured":"Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. In: 7th Systems Software Verification, Sydney, Australia, pp. 1\u201310, November 2012"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Delaware, B., Keuchel, S., Schrijvers, T., d. S. Oliveira, B.C.: Modular monadic meta-theory. In: ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), Boston, MA, USA, 25\u201327 September 2013, pp. 319\u2013330 (2013)","DOI":"10.1145\/2544174.2500587"},{"issue":"4\u20135","key":"9_CR10","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1017\/S0956796811000189","volume":"21","author":"S Fischer","year":"2011","unstructured":"Fischer, S., Kiselyov, O., Shan, C.: Purely functional lazy nondeterministic programming. J. Funct. Program. 21(4\u20135), 413\u2013465 (2011)","journal-title":"J. Funct. Program."},{"key":"9_CR11","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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-35705-3_2","volume-title":"Unifying Theories of Programming","author":"J Gibbons","year":"2013","unstructured":"Gibbons, J.: Unifying theories of programming\u00a0with\u00a0monads. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 23\u201367. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-35705-3_2"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), Tokyo, Japan, 19\u201321 September 2011, pp. 2\u201314. ACM (2011)","DOI":"10.1145\/2034773.2034777"},{"issue":"2","key":"9_CR14","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formaliz. Reasoning 3(2), 95\u2013152 (2010)","journal-title":"J. Formaliz. Reasoning"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-642-32347-8_25","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2012","unstructured":"Gonthier, G., Tassi, E.: A language of patterns for subterm selection. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 361\u2013376. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-32347-8_25"},{"key":"9_CR16","unstructured":"Greenaway, D.: Automated Proof-Producing Abstraction of C Code. Ph.D. thesis, University of New South Wales, Sydney, Australia, January 2015"},{"issue":"5","key":"9_CR17","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1016\/j.ic.2009.07.003","volume":"208","author":"A Hirschowitz","year":"2010","unstructured":"Hirschowitz, A., Maggesi, M.: Modules over monads and initial semantics. Inf. Comput. 208(5), 545\u2013564 (2010)","journal-title":"Inf. Comput."},{"key":"9_CR18","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. IFIP AICT, vol. 323, pp. 1\u201319. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-15240-5_1"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/j.scico.2017.06.012","volume":"162","author":"N Jomaa","year":"2018","unstructured":"Jomaa, N., Nowak, D., Grimaud, G., Hym, S.: Formal proof of dynamic memory isolation based on MMU. Sci. Comput. Program. 162, 76\u201392 (2018)","journal-title":"Sci. Comput. Program."},{"key":"9_CR20","unstructured":"Jomaa, N., Torrini, P., Nowak, D., Grimaud, G., Hym, S.: Proof-oriented design of a separation kernel with minimal trusted computing base. In: 18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018), July 2018. Oxford, UK. Electronic Communications of the EASST Open Access Journal (2018)"},{"key":"9_CR21","unstructured":"Jones, M.P., Duponcheel, L.: Composing monads. Technical report YALEU\/DCS\/RR-1004, Yale University (Dec 1993)"},{"key":"9_CR22","series-title":"Workshops in Computing","first-page":"134","volume-title":"Functional Programming, Glasgow 1992","author":"DJ King","year":"1992","unstructured":"King, D.J., Wadler, P.: Combining monads. In: Launchbury, J., Sansom, P. (eds.) Functional Programming, Glasgow 1992. Workshops in Computing, pp. 134\u2013143. Springer, London (1992)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-319-95582-7_20","volume-title":"Formal Methods","author":"T Letan","year":"2018","unstructured":"Letan, T., R\u00e9gis-Gianas, Y., Chifflier, P., Hiet, G.: Modular verification of programs with effects and effect handlers in Coq. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 338\u2013354. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-95582-7_20"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-319-43144-4_16","volume-title":"Interactive Theorem Proving","author":"A Lochbihler","year":"2016","unstructured":"Lochbihler, A., Schneider, J.: Equational reasoning with applicative functors. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 252\u2013273. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-43144-4_16"},{"key":"9_CR25","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8","volume-title":"Categories for the Working Mathematician","year":"1978","unstructured":"Mac Lane, S. (ed.): Categories for the Working Mathematician. GTM, vol. 5. Springer, New York (1978). \n                    https:\/\/doi.org\/10.1007\/978-1-4757-4721-8"},{"key":"9_CR26","unstructured":"Mahboubi, A., Tassi, E.: Mathematical Components (2016). \n                    https:\/\/math-comp.github.io\/mcb\/\n                    \n                  , with contributions by Yves Bertot and Georges Gonthier. Version of 2018\/08\/11"},{"key":"9_CR27","unstructured":"Martin-Dorel, E., Tassi, E.: SSReflect in Coq 8.10. In: The Coq Workshop 2019, Portland, OR, USA, 8 September 2019, pp. 1\u20132, September 2019"},{"key":"9_CR28","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: LICS, pp. 14\u201323. IEEE Computer Society (1989)"},{"key":"9_CR29","unstructured":"Mu, S.C.: Functional pearls, reasoning and derivation of monadic programs, a case study of non-determinism and state, July 2017, draft. \n                    http:\/\/flolac.iis.sinica.edu.tw\/flolac18\/files\/test.pdf\n                    \n                  . Accessed 10 July 2019"},{"key":"9_CR30","unstructured":"Mu, S.C.: Calculating a backtracking algorithm: an exercise in monadic program derivation. Technical report TR-IIS-19-003, Institute of Information Science, Academia Sinica, June 2019"},{"key":"9_CR31","unstructured":"Mu, S.C.: Equational reasoning for non-deterministic monad: a case study of Spark aggregation. Technical report TR-IIS-19-002, Institute of Information Science, Academia Sinica, June 2019"},{"issue":"5","key":"9_CR32","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1017\/S0956796809007345","volume":"19","author":"S Mu","year":"2009","unstructured":"Mu, S., Ko, H., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19(5), 545\u2013579 (2009)","journal-title":"J. Funct. Program."},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 1988), Atlanta, GA, USA, 22\u201324 June 1988, pp. 199\u2013208. ACM (1988)","DOI":"10.1145\/960116.54010"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"90","DOI":"10.4204\/EPTCS.76.8","volume":"76","author":"Maciej Pir\u00f3g","year":"2012","unstructured":"Pir\u00f3g, M., Gibbons, J.: Tracing monadic computations and representing effects. In: 4th Workshop on Mathematically Structured Functional Programming (MSFP 2012). EPTCS, Tallinn, Estonia, 25 March 2012, vol. 76, pp. 90\u2013111 (2012)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45931-6_24","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2002","unstructured":"Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 342\u2013356. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45931-6_24"},{"key":"9_CR36","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2015.12.003","volume":"319","author":"M Pretnar","year":"2015","unstructured":"Pretnar, M.: An introduction to algebraic effects and handlers (invited tutorial paper). Electr. Notes Theor. Comput. Sci. 319, 19\u201335 (2015)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9_CR37","unstructured":"Shan, C.C.: Equational reasoning for probabilistic programming. In: POPL 2018 TutorialFest, January 2018"},{"issue":"1","key":"9_CR38","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."},{"key":"9_CR39","unstructured":"Voevodsky, V., Ahrens, B., Grayson, D., et al.: UniMath-a computer-checked library of univalent mathematics. \n                    https:\/\/github.com\/UniMath\/UniMath"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Comprehending monads. In: LISP and Functional Programming, pp. 61\u201378 (1990)","DOI":"10.1145\/91556.91592"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-33636-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:11:09Z","timestamp":1571479869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-33636-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030336356","9783030336363"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-33636-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MPC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Mathematics of Program Construction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","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":"mpc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.nott.ac.uk\/~pszgmh\/mpc19.html","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":"22","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":"0","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":"68% - 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":"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)"}}]}}