{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:27Z","timestamp":1725564567616},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_4","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T07:33:53Z","timestamp":1283672033000},"page":"30-43","source":"Crossref","is-referenced-by-count":7,"title":["Construction of a Semantic Model for a Typed Assembly Language"],"prefix":"10.1007","author":[{"given":"Gang","family":"Tan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar N.","family":"Swadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dinghao","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","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":"4_CR2","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":"#cr-split#-4_CR3.1","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., Zdancewic, S.: TALx86:A realistic typed assembly language. In: Second ACMSIGPLAN Workshop on Compiler Support for System Software, Atlanta, GA, pp. 25???35 (1999);","DOI":"10.21236\/ADA358572"},{"key":"#cr-split#-4_CR3.2","unstructured":"INRIA Technical Report 0288 (March 1999)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"League, C., Shao, Z., Trifonov, V.: Precision in practice: A type-preserving Java compiler. In: Proc. Int\u2019l. Conf. on Compiler Construction (2003)","DOI":"10.1007\/3-540-36579-6_8"},{"key":"4_CR5","volume-title":"Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2000)","author":"C. Colby","year":"2000","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Cline, K., Plesko, M.: A certifying compiler for Java. In: Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2000), ACM Press, New York (2000)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound TAL for back-end optimization. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2003), pp. 208\u2013219 (2003)","DOI":"10.1145\/781131.781155"},{"key":"4_CR7","volume-title":"Denotational Semantics: A Methodology for Language Development","author":"D.A. Schmidt","year":"1986","unstructured":"Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Boston (1986)"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/325694.325727","volume-title":"POPL 2000: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"A.W. Appel","year":"2000","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proofcarrying code. In: POPL 2000: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 243\u2013253. ACM Press, New York (2000)"},{"key":"4_CR9","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 proofcarrying code. ACM Trans. on Programming Languages and Systems\u00a023, 657\u2013683 (2001)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Appel, A.W., Virga, R.: Astratified semantics of general references embeddable in higher-order logic. In: 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 75\u201386 (2002)","DOI":"10.1109\/LICS.2002.1029818"},{"key":"4_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/10721959_2","volume-title":"Automated Deduction - CADE-17","author":"N.G. Michael","year":"2000","unstructured":"Michael, N.G., Appel, A.W.: Machine instruction syntax and semantics in higher-order logic. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 7\u201324. Springer, Heidelberg (2000)"},{"key":"4_CR12","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":"4_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"4_CR14","first-page":"387","volume-title":"Current Trends in Hardware Verification and Automatic Theorem Proving","author":"M. Gordon","year":"1988","unstructured":"Gordon, M.: Mechanizing programming logics in higher-order logic. In: Birtwistle, G.M., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automatic Theorem Proving, Banff, Canada, pp. 387\u2013439. Springer, Berlin (1988)"},{"key":"4_CR15","unstructured":"Wahab, M.: Verification and abstraction of flow-graph programs with pointers and computed jumps. Research Report CS-RR-354, Department of Computer Science, University of Warwick, Coventry, UK (1998)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Hamid, N., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 89\u2013100 (2002)","DOI":"10.1109\/LICS.2002.1029819"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1145\/604131.604149","volume-title":"The 30th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages","author":"K. Crary","year":"2003","unstructured":"Crary, K.: Toward a foundational typed assembly language. In: The 30th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 198\u2013212. ACM Press, New York (2003)"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115, 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"4_CR19","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"}],"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\/978-3-540-24622-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T13:41:03Z","timestamp":1559569263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}