{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:35Z","timestamp":1763467775410},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540489375"},{"type":"electronic","value":"9783540489382"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11924661_6","type":"book-chapter","created":{"date-parts":[[2006,10,27]],"date-time":"2006-10-27T09:42:39Z","timestamp":1161942159000},"page":"97-113","source":"Crossref","is-referenced-by-count":1,"title":["Proof Abstraction for Imperative Languages"],"prefix":"10.1007","author":[{"given":"William L.","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Sabry, A.: Correctness of monadic state: an imperative call-by-need calculus. In: Conference Record of POPL 1998: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, New York, NY, pp. 62\u201373 (1998)","DOI":"10.1145\/268946.268952"},{"key":"6_CR2","unstructured":"Espinosa, D.: Semantic Lego. PhD thesis, Columbia University (1995)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-45931-6_11","volume-title":"Foundations of Software Science and Computation Structures","author":"C. F\u00fchrmann","year":"2002","unstructured":"F\u00fchrmann, C.: Varieties of effects. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 144\u2013158. Springer, Heidelberg (2002)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Ghani, N., L\u00fcth, C.: Composing monads using coproducts. In: ACM International Conference on Functional Programming, pp. 133\u2013144 (2002)","DOI":"10.1145\/583852.581492"},{"key":"6_CR5","first-page":"11","volume-title":"Proceedings of the 1982 Symposium on Security and Privacy (SSP 1982)","author":"J.A. Goguen","year":"1990","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the 1982 Symposium on Security and Privacy (SSP 1982), pp. 11\u201320. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"6_CR6","unstructured":"Harrison, W.: Modular Compilers and Their Correctness Proofs. PhD thesis, University of Illinois at Urbana-Champaign (2001)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Harrison, W., Hook, J.: Achieving information flow security through precise control of effects. In: 18th IEEE Computer Security Foundations Workshop (CSFW 2005) (June 2005)","DOI":"10.1109\/CSFW.2005.6"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/10722010_14","volume-title":"Mathematics of Program Construction","author":"W. Harrison","year":"2000","unstructured":"Harrison, W., Kamin, S.: Metacomputation-based compiler architecture. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 213\u2013229. Springer, Heidelberg (2000)"},{"issue":"10","key":"6_CR9","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"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic\u00a01(1), 60\u201376 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Launchbury, J., Sabry, A.: Monadic state: Axiomatization and type safety. In: ACM SIGPLAN International Conference on Functional Programming, pp. 227\u2013238 (1997)","DOI":"10.1145\/258948.258970"},{"key":"6_CR12","series-title":"Foundations of Computing Series","volume-title":"Realistic Compiler Generation","author":"P. Lee","year":"1989","unstructured":"Lee, P.: Realistic Compiler Generation. Foundations of Computing Series. MIT Press, Cambridge (1989)"},{"key":"6_CR13","unstructured":"Liang, S.: Modular Monadic Semantics and Compilation. PhD thesis, Yale University (1997)"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/199448.199528","volume-title":"Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"S. Liang","year":"1995","unstructured":"Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 333\u2013343. ACM Press, New York (1995)"},{"key":"6_CR15","series-title":"Wiley-Teubner Series in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-96753-4","volume-title":"The Foundations of Program Verification","author":"J. Loeckx","year":"1987","unstructured":"Loeckx, J., Sieber, K., Stansifer, R.D.: The Foundations of Program Verification, 2nd edn. Wiley-Teubner Series in Computer Science. Wiley, Chichester (1987)","edition":"2"},{"key":"6_CR16","series-title":"Formal Models and Semantics","first-page":"365","volume-title":"Handbook of Theoretical Computer Science","author":"J.C. Mitchell","year":"1990","unstructured":"Mitchell, J.C.: Type systems for programming languages, In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 8. Formal Models and Semantics, vol.\u00a0B, pp. 365\u2013458. North-Holland, New York (1990)"},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","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. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"6_CR18","unstructured":"Moggi, E.: Personal communication with author"},{"key":"6_CR19","unstructured":"Moggi, E.: Representing program logics in evaluation logic (unpublished manuscript), available online (1994)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Moggi, E.: A semantics for evaluation logic. FUNDINF: Fundamenta Informatica\u00a022 (1995)","DOI":"10.3233\/FI-1995-22126"},{"key":"6_CR21","unstructured":"Moggi, E.: An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Dept. of Computer Science, Edinburgh Univ., 90"},{"key":"6_CR22","series-title":"Number\u00a026 in Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569869","volume-title":"Action Semantics","author":"P.D. Mosses","year":"1992","unstructured":"Mosses, P.D.: Action Semantics. Number\u00a026 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1992)"},{"issue":"2-4","key":"6_CR23","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0020-0190(00)00215-5","volume":"77","author":"D.A. Naumann","year":"2001","unstructured":"Naumann, D.A.: Calculating sharp adaptation rules. Information Processing Letters\u00a077(2-4), 201\u2013208 (2001)","journal-title":"Information Processing Letters"},{"key":"6_CR24","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-1-4471-3182-3_11","volume-title":"IVth Higher Order Workshop, Banff 1990, Workshops in Computing","author":"A.M. Pitts","year":"1991","unstructured":"Pitts, A.M.: Evaluation logic. In: Birtwistle, G. (ed.) IVth Higher Order Workshop, Banff 1990, Workshops in Computing, pp. 162\u2013189. Springer, Berlin (1991)"},{"key":"6_CR25","doi-asserted-by":"publisher","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. Applied Categorical Structures\u00a011, 69\u201394 (2003)","journal-title":"Applied Categorical Structures"},{"key":"6_CR26","volume-title":"The Craft of Programming","author":"J.C. Reynolds","year":"1981","unstructured":"Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-36578-8_19","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Schr\u00f6der","year":"2003","unstructured":"Schr\u00f6der, L., Mossakowski, T.: Monad-independent hoare logic in HASCASL. In: Pezz\u00e9, M. (ed.) FASE 2003. LNCS, vol.\u00a02621, pp. 261\u2013277. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11924661_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:59:42Z","timestamp":1605625182000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11924661_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540489375","9783540489382"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11924661_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}