{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:31Z","timestamp":1763468131657,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642370748"},{"type":"electronic","value":"9783642370755"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37075-5_17","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:37:23Z","timestamp":1361216243000},"page":"257-272","source":"Crossref","is-referenced-by-count":15,"title":["Separation Logic for Non-local Control Flow and Block Scope Variables"],"prefix":"10.1007","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[]},{"given":"Freek","family":"Wiedijk","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Appel, A.W.: Tactics for Separation Logic (2006), http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf"},{"key":"17_CR2","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":"A.W. 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.\u00a04732, pp. 5\u201321. Springer, Heidelberg (2007)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI, pp. 234\u2013245. ACM (2011)","DOI":"10.1145\/1993316.1993526"},{"issue":"3","key":"17_CR4","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/362929.362947","volume":"11","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Go To statement considered harmful. Communications of the ACM\u00a011(3), 147\u2013148 (1968); Letter to the Editor","journal-title":"Communications of the ACM"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544 (2012)","DOI":"10.1145\/2103621.2103719"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science\u00a0103(2), 235\u2013271 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"17_CR7","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G.P. Huet","year":"1997","unstructured":"Huet, G.P.: The Zipper. Journal of Functional Programming\u00a07(5), 549\u2013554 (1997)","journal-title":"Journal of Functional Programming"},{"key":"17_CR8","unstructured":"International Organization for Standardization. ISO\/IEC 9899-2011: Programming languages \u2013 C. ISO Working Group 14 (2012)"},{"key":"17_CR9","unstructured":"Knuth, D.: Structured programming with go to statements. In: Classics in software engineering, pp. 257\u2013321. Yourdon Press (1979)"},{"key":"17_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-22673-1_28","volume-title":"Intelligent Computer Mathematics","author":"R. Krebbers","year":"2011","unstructured":"Krebbers, R., Wiedijk, F.: A Formalization of the C99 Standard in HOL, Isabelle and Coq. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS (LNAI), vol.\u00a06824, pp. 301\u2013303. Springer, Heidelberg (2011)"},{"issue":"4","key":"17_CR11","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR12","unstructured":"Leroy, X.: The CompCert verified compiler, software and commented proof (2012), http:\/\/compcert.inria.fr\/"},{"key":"17_CR13","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-46691-6_13","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"D. Oheimb von","year":"1999","unstructured":"von Oheimb, D.: Hoare Logic for Mutual Recursion and Local Variables. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FSTTCS 1999. LNCS, vol.\u00a01738, pp. 168\u2013180. Springer, Heidelberg (1999)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as Resource in Hoare Logics. In: LICS, pp. 137\u2013146 (2006)","DOI":"10.1109\/LICS.2006.52"},{"issue":"4","key":"17_CR17","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science\u00a021(4), 795\u2013825 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR18","unstructured":"Tews, H.: Verifying Duff\u2019s device: A simple compositional denotational semantics for Goto and computed jumps (2004)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37075-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:32:42Z","timestamp":1745962362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37075-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370748","9783642370755"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37075-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}