{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:53Z","timestamp":1780994753557,"version":"3.54.1"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,3,1]],"date-time":"2010-03-01T00:00:00Z","timestamp":1267401600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100005076","name":"ARDA","doi-asserted-by":"crossref","award":["NBCHC030106"],"award-info":[{"award-number":["NBCHC030106"]}],"id":[{"id":"10.13039\/501100005076","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["F30602-99-1-0519"],"award-info":[{"award-number":["F30602-99-1-0519"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-9974553CCR-0208601CCF-0540914"],"award-info":[{"award-number":["CCR-9974553CCR-0208601CCF-0540914"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCR-9974553CCR-0208601CCF-0540914"],"award-info":[{"award-number":["CCR-9974553CCR-0208601CCF-0540914"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,3]]},"abstract":"<jats:p>\n            Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>\n              <jats:italic>c<\/jats:italic>\n            <\/jats:sub>\n            , a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and\n            <jats:italic>L<\/jats:italic>\n            <jats:sub>\n              <jats:italic>c<\/jats:italic>\n            <\/jats:sub>\n            to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler.\n          <\/jats:p>\n          <jats:p>\n            To prove the soundness of the TML type system we have successfully applied a new approach, that of\n            <jats:italic>step-indexed logical relations<\/jats:italic>\n            . This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.\n          <\/jats:p>","DOI":"10.1145\/1709093.1709094","type":"journal-article","created":{"date-parts":[[2010,3,16]],"date-time":"2010-03-16T19:25:36Z","timestamp":1268767536000},"page":"1-67","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Semantic foundations for typed assembly languages"],"prefix":"10.1145","volume":"32","author":[{"given":"Amal","family":"Ahmed","sequence":"first","affiliation":[{"name":"Princeton University, Princeton NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christina D.","family":"Richards","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kedar N.","family":"Swadi","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gang","family":"Tan","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel C.","family":"Wang","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,3,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Abadi M. and Cardelli L. 1996. A Theory of Objects. Springer New York.","DOI":"10.5555\/547964"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/788020.788891"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328476"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664579"},{"key":"e_1_2_1_6_1","unstructured":"Ahmed A. Appel A. W. and Virga R. 2003. An indexed model of impredicative polymorphism and mutable references. http:\/\/www.cs.princeton.edu\/~appel\/papers\/impred.pdf."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411227"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086376"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1365997.1366003"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781146"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318661"},{"key":"e_1_2_1_13_1","unstructured":"Appel A. W. 2000. Hints on proving theorems in Twelf. www.cs.princeton.edu\/~appel\/twelf-tutorial."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325727"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54444-5_83"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021013.61329.58"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264021"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_8"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273922"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Birkedal L. and Harper R. 1997. Relational interpretations of recursive types in an operational setting. In Theoretical Aspects of Computer Software. Springer Berlin.","DOI":"10.5555\/645869.668661"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_5"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263735"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781155"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288686"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349315"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351247"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604149"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 19th International Conference on Automated Deduction (CADE'03)","author":"Crary K.","unstructured":"Crary, K. and Sarkar, S. 2003. Foundational certified code in a metalogical framework. In Proceedings of the 19th International Conference on Automated Deduction (CADE'03). Springer, Berlin, 106--120."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264536"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190325"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292563"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664592"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_46_1","volume-title":"Informal Proceedings of the Workshop on Foundations of Object-Oriented Languages (FOOL).","author":"Hri\u0163cu C.","unstructured":"Hri\u0163cu, C. and Schwinghammer, J. 2008. A step-indexed semantics of imperative objects. In Informal Proceedings of the Workshop on Foundations of Object-Oriented Languages (FOOL)."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289468"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737411"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","unstructured":"MacQueen D. Plotkin G. and Sethi R. 1986. An ideal model for recursive polymophic types. Inf. Comput. 71 1\/2 95--130. 10.1016\/S0019-9958(86)80019-5","DOI":"10.1016\/S0019-9958(86)80019-5"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792881"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964006"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/648236.761384"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 2nd ACM SIGPLAN Workshop on Compiler Support for System Software. ACM Press","author":"Morrisett G.","unstructured":"Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., and Zdancewic, S. 1999a. TALx86: A realistic typed assembly language. In Proceedings of the 2nd ACM SIGPLAN Workshop on Compiler Support for System Software. ACM Press, New York, 25--35."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004178"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/358728.358748"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753634"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.5555\/646252.686023"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/647424.725796"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/645722.666533"},{"key":"e_1_2_1_67_1","volume-title":"Lambda-Definability and logical relations. Memo. SAI--RM--4","author":"Plotkin G. D.","unstructured":"Plotkin, G. D. 1973. Lambda-Definability and logical relations. Memo. SAI--RM--4, University of Edinburgh, Edinburgh, Scotland."},{"key":"e_1_2_1_68_1","volume-title":"The essence of Algol","author":"Reynolds J. C.","unstructured":"Reynolds, J. C. 1981. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, Eds. North-Holland, Amsterdam, 345--372."},{"key":"e_1_2_1_70_1","volume-title":"Proceedings of the 2nd Workshop on Structured Operational Semantics (SOS'05)","author":"Saabas A.","unstructured":"Saabas, A. and Uustalu, T. 2005. A compositional natural semantics and Hoare logic for low-level languages. In Proceedings of the 2nd Workshop on Structured Operational Semantics (SOS'05)."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_2_1_72_1","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Types in Compilation. ACM Press","author":"Shao Z.","year":"1997","unstructured":"Shao, Z. 1997. An overview of the FLINT\/ML compiler. In Proceedings of the ACM SIGPLAN Workshop on Types in Compilation. ACM Press, New York."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_2_1_75_1","volume-title":"Typed machine language. Tech. rep. TR-676-03","author":"Swadi K.","unstructured":"Swadi, K. 2003. Typed machine language. Tech. rep. TR-676-03, Princeton University, Princeton, New Jersey."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/1104302"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_6"},{"key":"e_1_2_1_79_1","volume-title":"Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Compute Science","volume":"2937","author":"Tan G.","unstructured":"Tan, G., Appel, A. W., Swadi, K. N., and Wu, D. 2004. Construction of a semantic model for a typed assembly language. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Compute Science, vol. 2937. Springer, Berlin, 30--43."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231414"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263755"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.5555\/1104490"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888276"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765712.1765739"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1709093.1709094","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1709093.1709094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:09Z","timestamp":1750278129000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1709093.1709094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":80,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["10.1145\/1709093.1709094"],"URL":"https:\/\/doi.org\/10.1145\/1709093.1709094","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3]]},"assertion":[{"value":"2006-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-06-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-03-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}