{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:59Z","timestamp":1761596939053},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_6","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"80-94","source":"Crossref","is-referenced-by-count":33,"title":["A Compositional Logic for Control Flow"],"prefix":"10.1007","author":[{"given":"Gang","family":"Tan","sequence":"first","affiliation":[]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","first-page":"578","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the Association for Computing Machinery\u00a012, 578\u2013580 (1969)","journal-title":"Communications of the Association for Computing Machinery"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"G. Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying code. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. on Programming Languages and Systems\u00a021, 527\u2013568 (1999)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/LICS.2001.932501","volume-title":"Symposium on Logic in Computer Science (LICS 2001)","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Symposium on Logic in Computer Science (LICS 2001), pp. 247\u2013258. IEEE, Los Alamitos (2001)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Clint, M., Hoare, C.A.R.: Program proving: Jumps and functions. Acta Informatica, 214\u2013224 (1972)","DOI":"10.1007\/BF00288686"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/BF00289468","volume":"7","author":"T. Kowaltowski","year":"1977","unstructured":"Kowaltowski, T.: Axiomatic approach to side effects and general jumps. Acta Informatica\u00a07, 357\u2013360 (1977)","journal-title":"Acta Informatica"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF00264021","volume":"11","author":"M. Arbib","year":"1979","unstructured":"Arbib, M., Alagic, S.: Proof rules for gotos. Acta Informatica\u00a011, 139\u2013148 (1979)","journal-title":"Acta Informatica"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/BF00264536","volume":"15","author":"A. Bruin de","year":"1981","unstructured":"de Bruin, A.: Goto statements: Semantics and deduction systems. Acta Informatica\u00a015, 385\u2013424 (1981)","journal-title":"Acta Informatica"},{"key":"6_CR9","doi-asserted-by":"crossref","first-page":"927","DOI":"10.1145\/358728.358748","volume":"25","author":"M.J. O\u2019Donnell","year":"1982","unstructured":"O\u2019Donnell, M.J.: A critique of the foundations of hoare style programming logics. Communications of the Association for Computing Machinery\u00a025, 927\u2013935 (1982)","journal-title":"Communications of the Association for Computing Machinery"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics, pp. 19\u201332. Providence, Rhode Island (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: Program fragments, linking, and modularization. In: 24th ACM Symposium on Principles of Programming Languages, pp. 266\u2013277 (1997)","DOI":"10.1145\/263699.263735"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Glew, N., Morrisett, G.: Type-safe linking and modular assembly language. In: 26th ACM Symposium on Principles of Programming Languages, pp. 250\u2013261 (1999)","DOI":"10.1145\/292540.292563"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: 3rd Asian Symposium on Programming Languages and Systems (2005)","DOI":"10.1007\/11575467_24"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: 33rd ACM Symposium on Principles of Programming Languages (2006) (to appear)","DOI":"10.1145\/1111037.1111066"},{"key":"6_CR15","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and Hoare logic for low-level languages. In: Proceedings of the Second Workshop on Structured Operational Semantics, SOS 2005 (2005)"},{"key":"6_CR16","unstructured":"Tan, G.: A Compositional Logic for Control Flow and its Application in Foundational Proof-Carrying Code. PhD thesis, Princeton University (2005)"},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. on Programming Languages and Systems\u00a023, 657\u2013683 (2001)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-24622-0_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Tan","year":"2004","unstructured":"Tan, G., Appel, A.W., Swadi, K.N., Wu, D.: Construction of a semantic model for a typed assembly language. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 30\u201343. Springer, Heidelberg (2004)"},{"key":"6_CR19","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard isomorphism. Available as DIKU Rapport 98\/14 (1998)"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing\u00a07, 70\u201390 (1978)","journal-title":"SIAM Journal on Computing"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound TAL for back-end optimization. In: ACM Conference on Programming Language Design and Implementation, pp. 208\u2013219 (2003)","DOI":"10.1145\/781131.781155"},{"key":"6_CR22","unstructured":"Swadi, K.N.: Typed Machine Language. PhD thesis, Princeton University (2003)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:07:05Z","timestamp":1619507225000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11609773_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}