{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T04:10:10Z","timestamp":1750479010746,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2005,1]]},"abstract":"<jats:p>\n            A\n            <jats:italic>certified binary<\/jats:italic>\n            is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In this article, we present a general framework for explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects while still maintaining decidable typechecking. We show how to integrate an entire proof system (the calculus of inductive constructions) into a compiler intermediate language and how the intermediate language can undergo complex transformations (CPS and closure conversion) while preserving proofs represented in the type system. Our work provides a foundation for the process of automatically generating certified binaries in a type-theoretic framework.\n          <\/jats:p>","DOI":"10.1145\/1053468.1053469","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["A type system for certified binaries"],"prefix":"10.1145","volume":"27","author":[{"given":"Zhong","family":"Shao","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valery","family":"Trifonov","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bratin","family":"Saha","sequence":"additional","affiliation":[{"name":"Intel Corporation, Santa Clara, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaos","family":"Papaspyrou","sequence":"additional","affiliation":[{"name":"National Technical University of Athens, Athens, Greece"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,1]]},"reference":[{"key":"e_1_2_1_2_1","article-title":"Models for security policies in proof-carrying code","author":"Appel A. W.","year":"2001","unstructured":"Appel , A. W. and Felten , E. W. 2001 . Models for security policies in proof-carrying code . Tech. Rep. CS-TR-636-01, Princeton Univ., Princeton, N.J. Appel, A. W. and Felten, E. W. 2001. Models for security policies in proof-carrying code. Tech. Rep. CS-TR-636-01, Princeton Univ., Princeton, N.J.","journal-title":"Tech. Rep. CS-TR-636-01, Princeton Univ., Princeton, N.J."},{"key":"e_1_2_1_3_1","first-page":"243","volume-title":"Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM","author":"Appel A. W.","unstructured":"Appel , A. W. and Felty , A. P . 2000. A semantic model of types and machine instructions for proof-carrying code . In Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM , New York , pp. 243 -- 253 . 10.1145\/325694.325727 Appel, A. W. and Felty, A. P. 2000. A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM, New York, pp. 243--253. 10.1145\/325694.325727"},{"volume-title":"Handbook of Logic in Computer Science","author":"Barendregt H. P.","key":"e_1_2_1_4_1","unstructured":"Barendregt , H. P. 1991. Lambda calculi with types . In Handbook of Logic in Computer Science , vol. 2 , S. Abramsky, D. Gabbay, and T. Maibaum, Eds. Oxford Univ. Press . Barendregt, H. P. 1991. Lambda calculi with types. In Handbook of Logic in Computer Science, vol. 2, S. Abramsky, D. Gabbay, and T. Maibaum, Eds. Oxford Univ. Press."},{"key":"e_1_2_1_5_1","unstructured":"Barendregt H. P. and Geuvers H. 1999. Proof-assistants using dependent type systems. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. Elsevier Amsterdam The Netherlands.   Barendregt H. P. and Geuvers H. 1999. Proof-assistants using dependent type systems. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. Elsevier Amsterdam The Netherlands."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000206149"},{"key":"e_1_2_1_7_1","volume-title":"Deliverables: An approach to program development in constructions. Tech. Rep. ECS-LFCS-91-133, Univ. of Edinburgh, UK.","author":"Burstall R.","year":"1991","unstructured":"Burstall , R. and McKinna , J. 1991 . Deliverables: An approach to program development in constructions. Tech. Rep. ECS-LFCS-91-133, Univ. of Edinburgh, UK. Burstall, R. and McKinna, J. 1991. Deliverables: An approach to program development in constructions. Tech. Rep. ECS-LFCS-91-133, Univ. of Edinburgh, UK."},{"volume-title":"Proceedings of the 11th IEEE Symposium on Logic in Computer Science. 264--275","author":"Cervesato I.","key":"e_1_2_1_8_1","unstructured":"Cervesato , I. and Pfenning , F . 1996. A linear logical framework . In Proceedings of the 11th IEEE Symposium on Logic in Computer Science. 264--275 . Cervesato, I. and Pfenning, F. 1996. A linear logical framework. In Proceedings of the 11th IEEE Symposium on Logic in Computer Science. 264--275."},{"volume-title":"Proceedings of the 2000 ACM Conference on Programming Language Design and Implementation. ACM","author":"Colby C.","key":"e_1_2_1_9_1","unstructured":"Colby , C. , Lee , P. , Necula , G. C. , Blau , F. , Plesko , M. , and Cline , K . 2000. A certifying compiler for Java . In Proceedings of the 2000 ACM Conference on Programming Language Design and Implementation. ACM , New York, 95--107. 10.1145\/349299.349315 Colby, C., Lee, P., Necula, G. C., Blau, F., Plesko, M., and Cline, K. 2000. A certifying compiler for Java. In Proceedings of the 2000 ACM Conference on Programming Language Design and Implementation. ACM, New York, 95--107. 10.1145\/349299.349315"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Constable R. 1985. Constructive mathematics as a programming logic I: Some principles of theory. Ann. Disc. Math. 24.  Constable R. 1985. Constructive mathematics as a programming logic I: Some principles of theory. Ann. Disc. Math. 24.","DOI":"10.1016\/S0304-0208(08)73073-1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_12_1","volume-title":"Tech. Rep. CMU-CS-01-113, School of Computer Science, Carnegie Mellon Univ.","author":"Crary K.","year":"2001","unstructured":"Crary , K. and Vanderwaart , J . 2001 . An expressive, scalable type theory for certified code. Tech. Rep. CMU-CS-01-113, School of Computer Science, Carnegie Mellon Univ. , Pittsburgh, Pa . Crary, K. and Vanderwaart, J. 2001. An expressive, scalable type theory for certified code. Tech. Rep. CMU-CS-01-113, School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa."},{"volume-title":"Proceedings of the 26th ACM Symposium on Principles of Programming Languages. ACM","author":"Crary K.","key":"e_1_2_1_13_1","unstructured":"Crary , K. , Walker , D. , and Morrisett , G . 1999. Typed memory management in a calculus of capabilities . In Proceedings of the 26th ACM Symposium on Principles of Programming Languages. ACM , New York, 262--275. 10.1145\/292540.292564 Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages. ACM, New York, 262--275. 10.1145\/292540.292564"},{"volume-title":"Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming. ACM","author":"Crary K.","key":"e_1_2_1_14_1","unstructured":"Crary , K. and Weirich , S . 1999. Flexible type analysis . In Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming. ACM , New York, 233--248. 10.1145\/317636.317906 Crary, K. and Weirich, S. 1999. Flexible type analysis. In Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming. ACM, New York, 233--248. 10.1145\/317636.317906"},{"volume-title":"Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM","author":"Crary K.","key":"e_1_2_1_15_1","unstructured":"Crary , K. and Weirich , S . 2000. Resource bound certification . In Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM , New York, 184--198. 10.1145\/325694.325716 Crary, K. and Weirich, S. 2000. Resource bound certification. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM, New York, 184--198. 10.1145\/325694.325716"},{"volume-title":"Proceedings of the 1998 ACM SIGPLAN Int'l Conf. on Functional Prog. ACM","author":"Crary K.","key":"e_1_2_1_16_1","unstructured":"Crary , K. , Weirich , S. , and Morrisett , G . 1998. Intensional polymorphism in type-erasure semantics . In Proceedings of the 1998 ACM SIGPLAN Int'l Conf. on Functional Prog. ACM , New York, 301--312. 10.1145\/289423.289459 Crary, K., Weirich, S., and Morrisett, G. 1998. Intensional polymorphism in type-erasure semantics. In Proceedings of the 1998 ACM SIGPLAN Int'l Conf. on Functional Prog. ACM, New York, 301--312. 10.1145\/289423.289459"},{"key":"e_1_2_1_19_1","volume-title":"Perlis Symposium","author":"Harper R.","year":"2000","unstructured":"Harper , R. 2000 . The practice of type theory. Talk presented at 2000 Alan J . Perlis Symposium , Yale University, New Haven, Conn. Harper, R. 2000. The practice of type theory. Talk presented at 2000 Alan J. Perlis Symposium, Yale University, New Haven, Conn."},{"volume-title":"Proceedings of the 20th ACM Symposium on Principles of Programming Languages. ACM","author":"Harper R.","key":"e_1_2_1_20_1","unstructured":"Harper , R. and Lillibridge , M . 1993. Explicit polymorphism and CPS conversion . In Proceedings of the 20th ACM Symposium on Principles of Programming Languages. ACM , New York, 206--219. 10.1145\/158511.158630 Harper, R. and Lillibridge, M. 1993. Explicit polymorphism and CPS conversion. In Proceedings of the 20th ACM Symposium on Principles of Programming Languages. ACM, New York, 206--219. 10.1145\/158511.158630"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 22nd ACM Symposium on Principles of Programming Languages. ACM","author":"Harper R.","year":"1994","unstructured":"Harper , R. and Morrisett , G . 1995. Compiling polymorphism using intensional type analysis . In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages. ACM , New York, 130--141. 10.1145\/ 1994 48.199475 Harper, R. and Morrisett, G. 1995. Compiling polymorphism using intensional type analysis. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages. ACM, New York, 130--141. 10.1145\/199448.199475"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Conference on Theoretical Aspects of Computer Software, A. R. Meyer, Ed. 701--730","author":"Hayashi S.","year":"1991","unstructured":"Hayashi , S. 1991 . Singleton, union and intersection types for program extraction . In Proceedings of the International Conference on Theoretical Aspects of Computer Software, A. R. Meyer, Ed. 701--730 . Hayashi, S. 1991. Singleton, union and intersection types for program extraction. In Proceedings of the International Conference on Theoretical Aspects of Computer Software, A. R. Meyer, Ed. 701--730."},{"volume-title":"To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism","author":"Howard W. A.","key":"e_1_2_1_23_1","unstructured":"Howard , W. A. 1980. The formulae-as-types notion of constructions . In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism . Academic Press , Orlando, Fla . Howard, W. A. 1980. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism. Academic Press, Orlando, Fla."},{"key":"e_1_2_1_24_1","unstructured":"Huet G. Paulin-Mohring C. etal 2000. The Coq proof assistant reference manual. Part of the Coq system version 6.3.1.  Huet G. Paulin-Mohring C. et al. 2000. The Coq proof assistant reference manual. Part of the Coq system version 6.3.1."},{"volume-title":"Proceedings of the 23rd ACM Symposium on Principles of Programming Languages. ACM","author":"Minamide Y.","key":"e_1_2_1_25_1","unstructured":"Minamide , Y. , Morrisett , G. , and Harper , R . 1996. Typed closure conversion . In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages. ACM , New York, 271--283. 10.1145\/237721.237791 Minamide, Y., Morrisett, G., and Harper, R. 1996. Typed closure conversion. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages. ACM, New York, 271--283. 10.1145\/237721.237791"},{"volume-title":"Proceedings of the 2001 ACM Conference on Programming Language Design and Implementation. ACM","author":"Monnier S.","key":"e_1_2_1_26_1","unstructured":"Monnier , S. , Saha , B. , and Shao , Z . 2001. Principled scavenging . In Proceedings of the 2001 ACM Conference on Programming Language Design and Implementation. ACM , New York, 81--91. 10.1145\/378795.378817 Monnier, S., Saha, B., and Shao, Z. 2001. Principled scavenging. In Proceedings of the 2001 ACM Conference on Programming Language Design and Implementation. ACM, New York, 81--91. 10.1145\/378795.378817"},{"volume-title":"Proceedings of the 25th ACM Symposium on Principles of Programming Languages. ACM","author":"Morrisett G.","key":"e_1_2_1_27_1","unstructured":"Morrisett , G. , Walker , D. , Crary , K. , and Glew , N . 1998. From System F to typed assembly language . In Proceedings of the 25th ACM Symposium on Principles of Programming Languages. ACM , New York, 85--97. 10.1145\/268946.268954 Morrisett, G., Walker, D., Crary, K., and Glew, N. 1998. From System F to typed assembly language. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages. ACM, New York, 85--97. 10.1145\/268946.268954"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 24th ACM Symposium on Principles of Programming Languages. ACM","author":"Necula G.","year":"1997","unstructured":"Necula , G. 1997 . Proof-carrying code . In Proceedings of the 24th ACM Symposium on Principles of Programming Languages. ACM , New York, 106--119. 10.1145\/263699.263712 Necula, G. 1997. Proof-carrying code. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages. ACM, New York, 106--119. 10.1145\/263699.263712"},{"volume-title":"Proceedings of the 2nd USENIX Symposium on Operating System Design and Implementation. USENIX Assoc., 229--243","author":"Necula G.","key":"e_1_2_1_30_1","unstructured":"Necula , G. and Lee , P . 1996. Safe kernel extensions without run-time checking . In Proceedings of the 2nd USENIX Symposium on Operating System Design and Implementation. USENIX Assoc., 229--243 . 10.1145\/238721.238781 Necula, G. and Lee, P. 1996. Safe kernel extensions without run-time checking. In Proceedings of the 2nd USENIX Symposium on Operating System Design and Implementation. USENIX Assoc., 229--243. 10.1145\/238721.238781"},{"volume-title":"Proceedings of the 1998 ACM Conference on Programming Language Design and Implementation. ACM","author":"Necula G.","key":"e_1_2_1_31_1","unstructured":"Necula , G. and Lee , P . 1998. The design and implementation of a certifying compiler . In Proceedings of the 1998 ACM Conference on Programming Language Design and Implementation. ACM , New York, 333--344. 10.1145\/277650.277752 Necula, G. and Lee, P. 1998. The design and implementation of a certifying compiler. In Proceedings of the 1998 ACM Conference on Programming Language Design and Implementation. ACM, New York, 333--344. 10.1145\/277650.277752"},{"key":"e_1_2_1_32_1","unstructured":"Nordstrom B. Petersson K. and Smith J. 1990. Programming in Martin-L\u00f6f's type theory. Oxford University Press.   Nordstrom B. Petersson K. and Smith J. 1990. Programming in Martin-L\u00f6f's type theory. Oxford University Press."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 16th ACM Symposium on Principles of Programming Languages. ACM","author":"Paulin-Mohring C.","year":"1989","unstructured":"Paulin-Mohring , C. 1989 . Extracting F\u03c9's programs from proofs in the Calculus of Constructions . In Proceedings of the 16th ACM Symposium on Principles of Programming Languages. ACM , New York, 89--104. 10.1145\/75277.75285 Paulin-Mohring, C. 1989. Extracting F\u03c9's programs from proofs in the Calculus of Constructions. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages. ACM, New York, 89--104. 10.1145\/75277.75285"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the TLCA, M. Bezem and J. Groote, Eds. Lecture Notes in Computer Science","volume":"664","author":"Paulin-Mohring C.","year":"1993","unstructured":"Paulin-Mohring , C. 1993 . Inductive definitions in the system Coq--Rules and properties . In Proceedings of the TLCA, M. Bezem and J. Groote, Eds. Lecture Notes in Computer Science , vol. 664 , Springer-Verlag, New York. Paulin-Mohring, C. 1993. Inductive definitions in the system Coq--Rules and properties. In Proceedings of the TLCA, M. Bezem and J. Groote, Eds. Lecture Notes in Computer Science, vol. 664, Springer-Verlag, New York."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 1997 ACM SIGPLAN Workshop on Types in Compilation. ACM","author":"Shao Z.","year":"1997","unstructured":"Shao , Z. 1997 . An overview of the FLINT\/ML compiler . In Proceedings of the 1997 ACM SIGPLAN Workshop on Types in Compilation. ACM , New York. Shao, Z. 1997. An overview of the FLINT\/ML compiler. In Proceedings of the 1997 ACM SIGPLAN Workshop on Types in Compilation. ACM, New York."},{"volume-title":"Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming. ACM","author":"Shao Z.","key":"e_1_2_1_36_1","unstructured":"Shao , Z. , League , C. , and Monnier , S . 1998. Implementing typed intermediate languages . In Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming. ACM , New York, 313--323. 10.1145\/289423.289460 Shao, Z., League, C., and Monnier, S. 1998. Implementing typed intermediate languages. In Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming. ACM, New York, 313--323. 10.1145\/289423.289460"},{"key":"e_1_2_1_37_1","volume-title":"Tech. Rep. YALEU\/DCS\/TR-1211, Dept. of Computer Science","author":"Shao Z.","year":"2001","unstructured":"Shao , Z. , Saha , B. , Trifonov , V. , and Papaspyrou , N . 2001 . A type system for certified binaries. Tech. Rep. YALEU\/DCS\/TR-1211, Dept. of Computer Science , Yale University, New Haven , Conn . Shao, Z., Saha, B., Trifonov, V., and Papaspyrou, N. 2001. A type system for certified binaries. Tech. Rep. YALEU\/DCS\/TR-1211, Dept. of Computer Science, Yale University, New Haven, Conn."},{"volume-title":"Proceedings of the 1990 ACM Conference on LISP and Functional Programming. ACM","author":"Sheldon M. A.","key":"e_1_2_1_38_1","unstructured":"Sheldon , M. A. and Gifford , D. K . 1990. Static dependent types for first class modules . In Proceedings of the 1990 ACM Conference on LISP and Functional Programming. ACM , New York, 20--29. 10.1145\/91556.91577 Sheldon, M. A. and Gifford, D. K. 1990. Static dependent types for first class modules. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming. ACM, New York, 20--29. 10.1145\/91556.91577"},{"volume-title":"Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming. ACM","author":"Trifonov V.","key":"e_1_2_1_39_1","unstructured":"Trifonov , V. , Saha , B. , and Shao , Z . 2000. Fully reflexive intensional type analysis . In Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming. ACM , New York, 82--93. 10.1145\/351240.351248 Trifonov, V., Saha, B., and Shao, Z. 2000. Fully reflexive intensional type analysis. In Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming. ACM, New York, 82--93. 10.1145\/351240.351248"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM","author":"Walker D.","year":"2000","unstructured":"Walker , D. 2000 . A type system for expressive security policies . In Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM , New York, 254--267. 10.1145\/325694.325728 Walker, D. 2000. A type system for expressive security policies. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages. ACM, New York, 254--267. 10.1145\/325694.325728"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"volume-title":"Proceedings of the 26th ACM Symposium on Principles of Programming Languages. ACM","author":"Xi H.","key":"e_1_2_1_43_1","unstructured":"Xi , H. and Pfenning , F . 1999. Dependent types in practical programming . In Proceedings of the 26th ACM Symposium on Principles of Programming Languages. ACM , New York, 214--227. 10.1145\/292540.292560 Xi, H. and Pfenning, F. 1999. Dependent types in practical programming. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages. ACM, New York, 214--227. 10.1145\/292540.292560"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1053468.1053469","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1053468.1053469","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:07:53Z","timestamp":1750262873000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1053468.1053469"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["10.1145\/1053468.1053469"],"URL":"https:\/\/doi.org\/10.1145\/1053468.1053469","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2005,1]]},"assertion":[{"value":"2005-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}