{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:30:55Z","timestamp":1770283855543,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_30","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"440-451","source":"Crossref","is-referenced-by-count":29,"title":["A Hoare Logic for the State Monad"],"prefix":"10.1007","author":[{"given":"Wouter","family":"Swierstra","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Munoz, C., Ait, O. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. Mathematical Aspects of Computer Science\u00a019 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"30_CR3","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"30_CR4","unstructured":"Hutton, G., Fulger, D.: Reasoning about effects: seeing the wood through the trees. In: Proceedings of the Ninth Symposium on Trends in Functional Programming (2008)"},{"key":"30_CR5","first-page":"42","volume-title":"POPL 2006: 33rd Symposium on Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006: 33rd Symposium on Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"30_CR6","first-page":"167","volume-title":"Proceedings of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages","author":"P. Martin-L\u00f6f","year":"1985","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Proceedings of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, pp. 167\u2013184. Prentice-Hall, Inc., Englewood Cliffs (1985)"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"McKinna, J.: Deliverables: a categorical approach to program development in type theory. Ph.D thesis, School of Informatics at the University of Edinburgh (1992)","DOI":"10.1007\/3-540-57182-5_3"},{"key":"30_CR8","unstructured":"Nanevski, A., Morrisett, G.: Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University (2005)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare Type Theory. In: ICFP 2006: Proceedings of the Eleventh ACM SIGPLAN Internation Conference on Functional Programming (2006)","DOI":"10.1145\/1159803.1159812"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: ICFP 2008: Proceedings of the Twelfth ACM SIGPLAN International Conference on Functional Programming (2008)","DOI":"10.1145\/1411204.1411237"},{"key":"30_CR11","volume-title":"Haskell 98 Language and Libraries: The Revised Report","year":"2003","unstructured":"Peyton Jones, S. (ed.): Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"30_CR13","unstructured":"Sozeau, M.: Un environnement pour la programmation avec types d\u00e9pendants. Ph.D thesis, Universit\u00e9 de Paris XI (2008)"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-74591-4_23","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Sprenger","year":"2007","unstructured":"Sprenger, C., Basin, D.: A monad-based modeling and verification toolbox with application to security protocols. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 302\u2013318. Springer, Heidelberg (2007)"},{"key":"30_CR15","unstructured":"The Coq development team. The Coq proof assistant reference manual. LogiCal Project, Version 8.2 (2008)"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The essence of functional programming. In: POPL 1992: Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1\u201314 (1992)","DOI":"10.1145\/143165.143169"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T02:48:23Z","timestamp":1558493303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}