{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T23:42:39Z","timestamp":1725925359956},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319720432"},{"type":"electronic","value":"9783319720449"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-72044-9_14","type":"book-chapter","created":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T09:14:43Z","timestamp":1512638083000},"page":"208-222","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Generic Hoare Logic for Order-Enriched Effects with Exceptions"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Rauch","sequence":"first","affiliation":[]},{"given":"Sergey","family":"Goncharov","sequence":"additional","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,8]]},"reference":[{"issue":"12","key":"14_CR1","doi-asserted-by":"crossref","first-page":"1306","DOI":"10.1016\/j.ic.2009.10.006","volume":"208","author":"J Ad\u00e1mek","year":"2010","unstructured":"Ad\u00e1mek, J., Milius, S., Velebil, J.: Equational properties of iterative monads. Inf. Comput. 208(12), 1306\u20131348 (2010)","journal-title":"Inf. Comput."},{"key":"14_CR2","volume-title":"Category Theory for Computing Science","year":"1995","unstructured":"Barr, M., Wells, C. (eds.): Category Theory for Computing Science, 2nd edn. Prentice Hall International (UK) Ltd., London (1995)","edition":"2"},{"key":"14_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-78034-9","volume-title":"Iteration Theories: The Equational Logic of Iterative Processes","author":"SL Bloom","year":"1993","unstructured":"Bloom, S.L., \u00c9sik, Z.: Iteration Theories: The Equational Logic of Iterative Processes. Springer-Verlag New York, Inc., New York (1993). \nhttps:\/\/doi.org\/10.1007\/978-3-642-78034-9"},{"key":"14_CR4","unstructured":"Cenciarelli, P., Moggi, E.: A syntactic approach to modularity in denotational semantics. In: Category Theory and Computer Science, CTCS 1993 (1993)"},{"issue":"8","key":"14_CR5","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Rauch, C., Schr\u00f6der, L.: Unguarded recursion on coinductive resumptions. In: Mathematical Foundations of Programming Semantics, MFPS 2015. ENTCS (2015)","DOI":"10.1016\/j.entcs.2015.12.012"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Schr\u00f6der, L.: A relatively complete Hoare logic for order-enriched effects. In: Logic in Computer Science, LICS 2013, pp. 273\u2013282. IEEE (2013)","DOI":"10.1109\/LICS.2013.33"},{"key":"14_CR8","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.tcs.2015.03.047","volume":"604","author":"I Hasuo","year":"2015","unstructured":"Hasuo, I.: Generic weakest precondition semantics from monads enriched with order. Theoret. Comput. Sci. 604, 2\u201329 (2015)","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284\u2013303. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/3-540-46428-X_20"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/BFb0013462","volume-title":"Category Theory and Computer Science","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: A modular approach to denotational semantics. In: Pitt, D.H., Curien, P.-L., Abramsky, S., Pitts, A.M., Poign\u00e9, A., Rydeheard, D.E. (eds.) CTCS 1991. LNCS, vol. 530, pp. 138\u2013139. Springer, Heidelberg (1991). \nhttps:\/\/doi.org\/10.1007\/BFb0013462"},{"key":"14_CR11","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93, 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"14_CR12","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-02571-6_12","volume-title":"Objects, Components, Models and Patterns","author":"M Nordio","year":"2009","unstructured":"Nordio, M., Calcagno, C., M\u00fcller, P., Meyer, B.: A sound and complete program logic for Eiffel. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol. 33, pp. 195\u2013214. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02571-6_12"},{"key":"14_CR13","doi-asserted-by":"crossref","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D Oheimb von","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concurr. Comput.: Pract. Exp. 13, 1173\u20131214 (2001)","journal-title":"Concurr. Comput.: Pract. Exp."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Pir\u00f3g, M., Gibbons, J.: The coinductive resumption monad. In: Mathematical Foundations of Programming Semantics, MFPS 2014. ENTCS, vol. 308, pp. 273\u2013288 (2014)","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"14_CR15","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1023\/A:1023064908962","volume":"11","author":"G Plotkin","year":"2003","unstructured":"Plotkin, G., Power, J.: Algebraic operations and generic effects. Appl. Categ. Struct. 11, 69\u201394 (2003)","journal-title":"Appl. Categ. Struct."},{"key":"14_CR16","unstructured":"Poetzsch-Heffter, A., Rauch, N.: Soundness and relative completeness of a programming logic for a sequential Java subset. Technical report, TU Kaiserlautern (2004)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-540-40020-2_25","volume-title":"Recent Trends in Algebraic Development Techniques","author":"L Schr\u00f6der","year":"2003","unstructured":"Schr\u00f6der, L., Mossakowski, T.: Monad-independent dynamic logic in HasCasl. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2002. LNCS, vol. 2755, pp. 425\u2013441. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-40020-2_25"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-27815-3_34","volume-title":"Algebraic Methodology and Software Technology","author":"L Schr\u00f6der","year":"2004","unstructured":"Schr\u00f6der, L., Mossakowski, T.: Generic exception handling and the Java monad. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 443\u2013459. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27815-3_34"},{"key":"14_CR19","unstructured":"Simpson, A.K.: Recursive types in Kleisli categories. Technical report, MFPS Tutorial, April 2007 (1992)"},{"key":"14_CR20","volume-title":"Topology via Logic","author":"S Vickers","year":"1989","unstructured":"Vickers, S.: Topology via Logic. Cambridge University Press, Cambridge (1989)"},{"key":"14_CR21","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1145\/262009.262011","volume":"29","author":"P Wadler","year":"1997","unstructured":"Wadler, P.: How to declare an imperative. ACM Comput. Surv. 29, 240\u2013263 (1997)","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72044-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T09:19:59Z","timestamp":1512638399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72044-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319720432","9783319720449"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72044-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}