{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:29Z","timestamp":1725568169850},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_9","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T09:13:30Z","timestamp":1288084410000},"page":"106-120","source":"Crossref","is-referenced-by-count":13,"title":["Foundational Certified Code in a Metalogical Framework"],"prefix":"10.1007","author":[{"given":"Karl","family":"Crary","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: Twenty-Seventh ACM Symposium on Principles of Programming Languages, Boston, January 2000, pp. 243\u2013253 (2000)","DOI":"10.1145\/325694.325727"},{"key":"9_CR2","unstructured":"Appel, A.W., Michael, N., Stump, A., Virga, R.: A trustworthy proof checker. Technical Report TR-647-02, Department of Computer Science, Princeton University (April 2002)"},{"key":"9_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45620-1_3","volume-title":"Automated Deduction - CADE-18","author":"A. Bernard","year":"2002","unstructured":"Bernard, A., Lee, P.: Temporal logic for proof-carrying code. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 31\u201346. Springer, Heidelberg (2002)"},{"issue":"9","key":"9_CR4","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1002\/spe.4380180902","volume":"18","author":"H.-J. Boehm","year":"1988","unstructured":"Boehm, H.-J., Weiser, M.: Garbage collection in an uncooperative environment. Software Practice and Experience\u00a018(9), 807\u2013820 (1988)","journal-title":"Software Practice and Experience"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Buyya, R., Baker, M. (eds.) GRID 2000. LNCS, vol.\u00a01971. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-44444-0"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/3-540-36133-2_11","volume-title":"Grid Computing - GRID 2002","author":"B.-Y.E. Chang","year":"2002","unstructured":"Chang, B.-Y.E., Crary, K., DeLap, M., Harper, R., Liszka, J., Murphy\u00f8 VII, T., Pfenning, F.: Trustless grid computing in conCert. In: Parashar, M. (ed.) GRID 2002. LNCS, vol.\u00a02536, pp. 112\u2013125. Springer, Heidelberg (2002)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G., Blau, F.: A certifying compiler for Java. In: 2000 SIGPLAN Conference on Programming Language Design and Implementation, Vancouver, British Columbia, June 2000, pp. 95\u2013107 (2000)","DOI":"10.1145\/349299.349315"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Crary, K.: Toward a foundational typed assembly language. In: Thirtieth ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, January 2003, pp. 198\u2013212 (2003)","DOI":"10.1145\/604131.604149"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Crary, K., Sarkar, S.: Foundational certified code in a metalogical framework. Technical Report CMU-CS-03-108, Carnegie Mellon University, School of Computer Science (2003)","DOI":"10.1007\/978-3-540-45085-6_9"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Hamid, N., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: Seventeenth IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, July 2002, pp. 89\u2013100 (2002)","DOI":"10.1109\/LICS.2002.1029819"},{"issue":"4","key":"9_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0020-0190(94)90120-1","volume":"51","author":"R. Harper","year":"1994","unstructured":"Harper, R.: A simplified account of polymorphic references. Information Processing Letters\u00a051(4), 201\u2013206 (1994); Follow-up note in Information Processing Letters 57(1) (1996)","journal-title":"Information Processing Letters"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"key":"9_CR13","unstructured":"Intel Corporation. IA-32 Intel Architecture Software Developer\u2019s Manual. Order numbers 245470\u2013245472 (2001)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Lee, C.A. (ed.) GRID 2001. LNCS, vol.\u00a02242. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45644-9"},{"key":"9_CR15","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1996","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Reading (1996)"},{"key":"9_CR16","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 Workshop on Compiler Support for System Software, Atlanta (May 1999)","DOI":"10.21236\/ADA358572"},{"issue":"1","key":"9_CR17","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1017\/S0956796801004178","volume":"12","author":"G. Morrisett","year":"2002","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. Journal of Functional Programming\u00a012(1), 43\u201388 (2002)","journal-title":"Journal of Functional Programming"},{"issue":"3","key":"9_CR18","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 Transactions on Programming Languages and Systems\u00a021(3), 527\u2013568 (1999); An earlier version appeared in the 1998 Symposium on Principles of Programming Languages","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Twenty-Fourth ACM Symposium on Principles of Programming Languages, Paris, January 1997, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: Second Symposium on Operating Systems Design and Implementation, Seattle, October 1996, pp. 229\u2013243 (1996)","DOI":"10.1145\/238721.238781"},{"key":"9_CR21","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania (September 1998)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Parashar, M. (ed.) GRID 2002. LNCS, vol.\u00a02536, Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-36133-2"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system coq \u2013 rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993)"},{"key":"9_CR24","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 \u2013 a metalogic framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"9_CR25","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: Twelf User\u2019s Guide, Version 1.3R4 (2002), Available electronically at http:\/\/www.cs.cmu.edu\/~twelf"},{"key":"9_CR26","unstructured":"SETI@Home (November 2000), http:\/\/setiathome.ssl.berkeley.edu"},{"key":"9_CR27","unstructured":"Tool Interface Standards Committee. Executable and Linking Format (ELF) specification (May 1995), http:\/\/x86.ddj.com\/ftp\/manuals\/tools\/elf.pdf"},{"key":"9_CR28","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"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T18:12:20Z","timestamp":1559758340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}