{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:08:28Z","timestamp":1774987708202,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,1,11]],"date-time":"2006-01-11T00:00:00Z","timestamp":1136937600000},"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":[],"published-print":{"date-parts":[[2006,1,11]]},"DOI":"10.1145\/1111037.1111066","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T10:52:40Z","timestamp":1139223160000},"page":"320-333","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["Certified assembly programming with embedded code pointers"],"prefix":"10.1145","author":[{"given":"Zhaozhong","family":"Ni","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789071"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604185"},{"key":"e_1_3_2_1_3_1","volume-title":"Princeton University","author":"Ahmed A. J.","year":"2004"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325727"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086401"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227603"},{"key":"e_1_3_2_1_9_1","unstructured":"B.-Y. E. Chang G. C. Necular and R. R. Schneck. Extensible code verification. Unpublished manuscript 2003.  B.-Y. E. Chang G. C. Necular and R. R. Schneck. Extensible code verification. Unpublished manuscript 2003."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781155"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349315"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604149"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581497"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086399"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_17_1","first-page":"143","volume-title":"Hoare","author":"Gordon M.","year":"1994"},{"key":"e_1_3_2_1_18_1","volume-title":"Addison-Wesley","author":"Gosling J.","year":"1996"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_10"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664592"},{"key":"e_1_3_2_1_21_1","unstructured":"H. Herbelin F. Kirchner B. Monate and J. Narboux. Faq about coq. http:\/\/pauillac.inria.fr\/coq\/doc\/faq.html#htoc38.  H. Herbelin F. Kirchner B. Monate and J. Narboux. Faq about coq. http:\/\/pauillac.inria.fr\/coq\/doc\/faq.html#htoc38."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013963.1013985"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.5"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00005-8"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_30_1","volume-title":"Carnegie Mellon Univ.","author":"Necula G.","year":"1998"},{"key":"e_1_3_2_1_31_1","first-page":"248","volume-title":"Proceedings of IEEE Symposium on Logic in Computer Science","author":"Necula G. C.","year":"2003"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Z. Ni and Z. Shao. Implementation for certified assembly programming with embedded code pointers. http:\/\/flint.cs.yale.edu\/publications\/xcap.html Oct. 2005.  Z. Ni and Z. Shao. Implementation for certified assembly programming with embedded code pointers. http:\/\/flint.cs.yale.edu\/publications\/xcap.html Oct. 2005.","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_2_1_33_1","volume-title":"Birkhauser","author":"O'Hearn P. W.","year":"1997"},{"key":"e_1_3_2_1_34_1","unstructured":"C.\n       \n      Paulin-Mohring\n    .\n      \n  \n   \n  Inductive definitions in the system Coq--rules and properties. In M. Bezem and J. Groote editors Proc. TLCA volume \n  664\n   of \n  LNCS\n  . \n  Springer-Verlag 1993\n  .   C. Paulin-Mohring. Inductive definitions in the system Coq--rules and properties. In M. Bezem and J. Groote editors Proc. TLCA volume 664 of LNCS. Springer-Verlag 1993."},{"key":"e_1_3_2_1_35_1","unstructured":"F. Pfenning. Automated theorem proving. http:\/\/www-2.cs.cmu.edu\/~fp\/courses\/atp\/ Apr. 2004.  F. Pfenning. Automated theorem proving. http:\/\/www-2.cs.cmu.edu\/~fp\/courses\/atp\/ Apr. 2004."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503293"},{"key":"e_1_3_2_1_39_1","volume-title":"Princeton University","author":"Tan G.","year":"2005"},{"key":"e_1_3_2_1_40_1","unstructured":"The Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.0 Oct. 2005.  The Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.0 Oct. 2005."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.01.003"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016875"},{"key":"e_1_3_2_1_45_1","unstructured":"Y. Yu . Automated Proofs of Object Code For A Widely Used Microprocessor. PhD thesis University of Texas at Austin 1992.   Y. Yu . Automated Proofs of Object Code For A Widely Used Microprocessor. PhD thesis University of Texas at Austin 1992."}],"event":{"name":"POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006","location":"Charleston South Carolina USA","acronym":"POPL06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111037.1111066","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1111037.1111066","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:38:28Z","timestamp":1750268308000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111037.1111066"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1,11]]},"references-count":45,"alternative-id":["10.1145\/1111037.1111066","10.1145\/1111037"],"URL":"https:\/\/doi.org\/10.1145\/1111037.1111066","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1111320.1111066","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,1,11]]},"assertion":[{"value":"2006-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}