{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:18:27Z","timestamp":1745986707008,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":55,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357046"},{"type":"electronic","value":"9783642357053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35705-3_2","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T01:49:52Z","timestamp":1357091392000},"page":"23-67","source":"Crossref","is-referenced-by-count":6,"title":["Unifying Theories of Programming\u00a0with\u00a0Monads"],"prefix":"10.1007","author":[{"given":"Jeremy","family":"Gibbons","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (1998), graduate Texts in Computer Science","key":"2_CR1","DOI":"10.1007\/978-1-4612-1674-2_1"},{"doi-asserted-by":"crossref","unstructured":"Beck, J.: Distributive laws. In: Seminar on Triples and Categorical Homology Theory. Lecture Notes in Mathematics, vol.\u00a080, pp. 119\u2013140. Springer (1969)","key":"2_CR2","DOI":"10.1007\/BFb0083084"},{"doi-asserted-by":"crossref","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall (1997)","key":"2_CR3","DOI":"10.1007\/978-3-642-61455-2_12"},{"unstructured":"Dean, J., Ghemawat, S.: MapReduce: Simplified data processing on large clusters. In: Operating Systems Design & Implementation, pp. 137\u2013150. USENIX Association (2004)","key":"2_CR4"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/j.entcs.2007.02.013","volume":"172","author":"Y. Deng","year":"2007","unstructured":"Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C., Zhang, C.: Remarks on testing probabilistic processes. Electronic Notes in Theoretical Computer Science\u00a0172, 359\u2013397 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall (1976)","key":"2_CR6"},{"doi-asserted-by":"crossref","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification. Springer (1985)","key":"2_CR7","DOI":"10.1007\/978-3-642-69962-7"},{"doi-asserted-by":"crossref","unstructured":"Eilenberg, S., Moore, J.C.: Adjoint functors and triples. Illinois Journal of Mathematics, 381\u2013398 (1965)","key":"2_CR8","DOI":"10.1215\/ijm\/1256068141"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0956796805005721","volume":"16","author":"M. Erwig","year":"2006","unstructured":"Erwig, M., Kollmansberger, S.: Probabilistic functional programming in Haskell. Journal of Functional Programming\u00a016(1), 21\u201334 (2006)","journal-title":"Journal of Functional Programming"},{"key":"2_CR10","first-page":"2","volume-title":"International Conference on Functional Programming","author":"J. Gibbons","year":"2011","unstructured":"Gibbons, J., Hinze, R.: Just do it: Simple monadic equational reasoning. In: Danvy, O. (ed.) International Conference on Functional Programming, pp. 2\u201314. ACM, New York (2011)"},{"doi-asserted-by":"crossref","unstructured":"Giry, M.: A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis. Lecture Notes in Mathematics, vol.\u00a0915, pp. 68\u201385. Springer (1981)","key":"2_CR11","DOI":"10.1007\/BFb0092872"},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"J. He","year":"1997","unstructured":"He, J., Seidel, K., McIver, A.: Probabilistic models for the Guarded Command Language. Science of Computer Programming\u00a028, 171\u2013192 (1997)","journal-title":"Science of Computer Programming"},{"issue":"2","key":"2_CR13","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/69610.357988","volume":"27","author":"E.C.R. Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming, parts\u00a0I and\u00a0II. Communications of the ACM\u00a027(2), 134\u2013151 (1984)","journal-title":"Communications of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Hinze, R.: Deriving backtracking monad transformers. In: International Conference on Functional Programming, pp. 186\u2013197 (2000)","key":"2_CR14","DOI":"10.1145\/357766.351258"},{"issue":"2","key":"2_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1002\/malq.19850310905","volume":"31","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: A couple of novelties in the propositional calculus. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik\u00a031(2), 173\u2013178 (1985)","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"issue":"1522","key":"2_CR16","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1098\/rsta.1984.0071","volume":"312","author":"C.A.R. Hoare","year":"1984","unstructured":"Hoare, C.A.R., Hanna, F.K.: Programs are predicates. Philosophical Transactions of the Royal Society, Part\u00a0A\u00a0312(1522), 475\u2013489 (1984)","journal-title":"Philosophical Transactions of the Royal Society, Part\u00a0A"},{"doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall (1998)","key":"2_CR17","DOI":"10.1007\/BFb0002714"},{"unstructured":"Hutton, G., Fulger, D.: Reasoning about effects: Seeing the wood through the trees. In: Preproceedings of Trends in Functional Programming (May 2008)","key":"2_CR18"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/j.entcs.2007.02.019","volume":"172","author":"M. Hyland","year":"2007","unstructured":"Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science\u00a0172, 437\u2013458 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Logic in Computer Science, pp. 186\u2013195 (1989)","key":"2_CR20","DOI":"10.1109\/LICS.1989.39173"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-03034-5_17","volume-title":"Domain-Specific Languages","author":"O. Kiselyov","year":"2009","unstructured":"Kiselyov, O., Shan, C.-c.: Embedded Probabilistic Programming. In: Taha, W.M. (ed.) DSL 2009. LNCS, vol.\u00a05658, pp. 360\u2013384. Springer, Heidelberg (2009)"},{"key":"2_CR22","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1090\/S0002-9939-1965-0177024-4","volume":"16","author":"H. Kleisli","year":"1965","unstructured":"Kleisli, H.: Every standard construction is induced by a pair of adjoint functors. Proceedings of the American Mathematical Society\u00a016, 544\u2013546 (1965)","journal-title":"Proceedings of the American Mathematical Society"},{"unstructured":"Knuth, D.E., Yao, A.C.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 357\u2013428. Academic Press (1976); reprinted in Selected Papers on Analysis of Algorithms (CSLI 2000)","key":"2_CR23"},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D. Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J.\u00a0Comput. Syst. Sci.\u00a022, 328\u2013350 (1981)","journal-title":"J.\u00a0Comput. Syst. Sci."},{"unstructured":"Launchbury, J.: Lazy imperative programming. In: ACM SIGPLAN Workshop on State in Programming Languages (June 1993)","key":"2_CR25"},{"doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Functorial Semantics of Algebraic Theories. Ph.D. thesis, Columbia University, also available with commentary as Theory and Applications of Categories Reprint 5 (1963), http:\/\/www.tac.mta.ca\/tac\/reprints\/articles\/5\/tr5abs.html","key":"2_CR26","DOI":"10.1073\/pnas.50.5.869"},{"unstructured":"Lawvere, F.W.: The category of probabilistic mappings (1962) (preprint)","key":"2_CR27"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-99902-4_3","volume-title":"Categorical Algebra","author":"F.E.J. Linton","year":"1966","unstructured":"Linton, F.E.J.: Some aspects of equational theories. In: Categorical Algebra, pp. 84\u201395. Springer, La Jolla (1966)"},{"unstructured":"Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes (1993) (manuscript) Oxford University Computing Laboratory","key":"2_CR29"},{"doi-asserted-by":"crossref","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Springer (1971)","key":"2_CR30","DOI":"10.1007\/978-1-4612-9839-7"},{"doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)","key":"2_CR31","DOI":"10.1145\/1059816.1059824"},{"key":"2_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/11591191_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A.K. McIver","year":"2005","unstructured":"McIver, A.K., Weber, T.: Towards Automated Proof Support for Probabilistic Distributed Systems. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 534\u2013548. Springer, Heidelberg (2005)"},{"unstructured":"McKinna, J.: Why dependent types matter. In: Principles of Programming Languages, p. 1. ACM (2006), full paper available at, http:\/\/www.cs.nott.ac.uk\/~txa\/publ\/ydtm.pdf","key":"2_CR33"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-009-0111-1","volume":"22","author":"L. Meinicke","year":"2010","unstructured":"Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. Formal Aspects of Computing\u00a022, 3\u201331 (2010)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-44618-4_26","volume-title":"CONCUR 2000 - Concurrency Theory","author":"M.W. Mislove","year":"2000","unstructured":"Mislove, M.W.: Nondeterminism and Probabilistic Choice: Obeying the Laws. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 350\u2013364. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation 93(1) (1991)","key":"2_CR36","DOI":"10.1016\/0890-5401(91)90052-4"},{"unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall (1994)","key":"2_CR37"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-31113-0_5","volume-title":"Mathematics of Program Construction","author":"C. Morgan","year":"2012","unstructured":"Morgan, C.: Elementary Probability Theory in the Eindhoven Style. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol.\u00a07342, pp. 48\u201373. Springer, Heidelberg (2012)"},{"issue":"6","key":"2_CR39","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/BF01213492","volume":"8","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing\u00a08(6), 617\u2013647 (1996)","journal-title":"Formal Aspects of Computing"},{"unstructured":"Peyton Jones, S.: Tackling the awkward squad: Monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Hoare, T., Broy, M., Steinbruggen, R. (eds.) Engineering Theories of Software Construction, pp. 47\u201396. IOS Press (2001)","key":"2_CR40"},{"doi-asserted-by":"crossref","unstructured":"Pir\u00f3g, M., Gibbons, J.: Tracing monadic computations and representing effects. In: Mathematically Structured Functional Programming (March 2012)","key":"2_CR41","DOI":"10.4204\/EPTCS.76.8"},{"key":"2_CR42","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.\u00a02303, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-00590-9_7","volume-title":"Programming Languages and Systems","author":"G. Plotkin","year":"2009","unstructured":"Plotkin, G., Pretnar, M.: Handlers of Algebraic Effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 80\u201394. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Principles of Programming Languages, pp. 154\u2013165 (2002)","key":"2_CR44","DOI":"10.1145\/565816.503288"},{"doi-asserted-by":"crossref","unstructured":"Rosenhouse, J.: The Monty Hall Problem: The Remarkable Story of Math\u2019s Most Contentious Brain Teaser. Oxford University Press (2009)","key":"2_CR45","DOI":"10.1093\/oso\/9780195367898.001.0001"},{"key":"2_CR46","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0167-6423(90)90056-J","volume":"14","author":"M. Spivey","year":"1990","unstructured":"Spivey, M.: A functional theory of exceptions. Science of Computer Programming\u00a014, 25\u201342 (1990)","journal-title":"Science of Computer Programming"},{"doi-asserted-by":"crossref","unstructured":"Spivey, M., Seres, S.: Combinators for logic programming. In: Gibbons, J., de Moor, O. (eds.) The Fun of Programming, pp. 177\u2013200. Cornerstones in Computing, Palgrave (2003)","key":"2_CR47","DOI":"10.1007\/978-1-349-91518-7_9"},{"issue":"7","key":"2_CR48","first-page":"751","volume":"10","author":"D.A. Turner","year":"2004","unstructured":"Turner, D.A.: Total functional programming. Journal of Universal Computer Science\u00a010(7), 751\u2013768 (2004)","journal-title":"Journal of Universal Computer Science"},{"key":"2_CR49","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 nondeterminism. Mathematical Structures in Computer Science\u00a016, 87\u2013113 (2006)","journal-title":"Mathematical Structures in Computer Science"},{"unstructured":"Vos Savant, M.: Ask Marilyn. Parade Magazine (September 9th, 1990), http:\/\/www.marilynvossavant.com\/articles\/gameshow.html","key":"2_CR50"},{"key":"2_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-15975-4_33","volume-title":"Functional Programming Languages and Computer Architecture","author":"P. Wadler","year":"1985","unstructured":"Wadler, P.: How to Replace Failure by a List of Successes: A Method for Exception Handling, Backtracking, and Pattern Matching in Lazy Functional Languages. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol.\u00a0201, pp. 113\u2013128. Springer, Heidelberg (1985), http:\/\/dx.doi.org\/10.1007\/3-540-15975-4_33"},{"unstructured":"Wadler, P.: Theorems for free? In: Functional Programming Languages and Computer Architecture, pp. 347\u2013359. ACM (1989), http:\/\/doi.acm.org\/10.1145\/99370.99404","key":"2_CR52"},{"issue":"4","key":"2_CR53","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1017\/S0960129500001560","volume":"2","author":"P. Wadler","year":"1992","unstructured":"Wadler, P.: Comprehending monads. Mathematical Structures in Computer Science\u00a02(4), 461\u2013493 (1992)","journal-title":"Mathematical Structures in Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Wadler, P.: Monads for functional programming. In: Broy, M. (ed.) Program Design Calculi: Proceedings of the Marktoberdorf Summer School (1992)","key":"2_CR54","DOI":"10.1007\/978-3-662-02880-3_8"},{"doi-asserted-by":"crossref","unstructured":"Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. In: Linn Jr., R.J., Uyar, M.\u00dc. (eds.) Protocol Specification, Testing and Verification, pp. 47\u201361. North-Holland (1992)","key":"2_CR55","DOI":"10.1016\/B978-0-444-89874-6.50010-6"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35705-3_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T15:33:12Z","timestamp":1745940792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35705-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642357046","9783642357053"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35705-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}