{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,11]],"date-time":"2024-12-11T05:55:06Z","timestamp":1733896506002,"version":"3.30.1"},"reference-count":32,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3850,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1016\/s0304-3975(01)00201-8","type":"journal-article","created":{"date-parts":[[2002,11,5]],"date-time":"2002-11-05T13:14:58Z","timestamp":1036502098000},"page":"1175-1199","source":"Crossref","is-referenced-by-count":6,"title":["Automated techniques for provably safe mobile code"],"prefix":"10.1016","volume":"290","author":[{"given":"Christopher","family":"Colby","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Crary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(01)00201-8_BIB1","series-title":"Proc. 6th Conf. on Computer and Communications Security","first-page":"52","article-title":"Proof-carrying authentication","author":"Appel","year":"1999"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB2","series-title":"Conf. Rec. 27th Ann. Symp. on Principles of Programming Languages (POPL\u201900)","first-page":"243","article-title":"A semantic model of types and machine instructions for proof-carrying code","author":"Appel","year":"2000"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB3","doi-asserted-by":"crossref","unstructured":"B. Bershad, S. Savage, P. Pardyak, E. Sirer, M. Fiuczynski, D. Becker, C. Chambers, S. Eggers, Extensibility, safety and performance in the SPIN operating system, Proc. 15th ACM Symp. on Operating Systems Principles, Copper Mountain, 1995, pp. 267\u2013284.","DOI":"10.1145\/224056.224077"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB4","doi-asserted-by":"crossref","unstructured":"C. Colby, P. Lee, G.C. Necula, F. Blau, M. Plesko, K. Cline, A certifying compiler for Java, Proc. Conf. on Programming Language Design and Implementation (PLDI\u201900), ACM Press, Vancouver, Canada, 2000, pp. 95\u2013107.","DOI":"10.1145\/349299.349315"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB5","doi-asserted-by":"crossref","unstructured":"K. Crary, S. Weirich, Resource bound certification, Proc. 27th ACM Symp. on Principles of Programming Languages, Boston, MA, 2000, pp. 184\u2013198.","DOI":"10.1145\/325694.325716"},{"issue":"1","key":"10.1016\/S0304-3975(01)00201-8_BIB6","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB7","unstructured":"R. Harper, F. Pfenning, On equivalence and canonical forms in the LF type theory, Technical Report CMU-CS-00-148, Department of Computer Science, Carnegie Mellon University, July 2000."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB8","unstructured":"S. Michaylov, F. Pfenning, An empirical study of the runtime behavior of higher-order logic programs, in: D. Miller (Ed.), Proc. Workshop on the \u03bbProlog Programming Language, University of Pennsylvania, Philadelphia, PA, 1992, pp. 257\u2013271, available as Technical Report MS-CIS-92-86."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB9","unstructured":"J.G. Morrisett, Compiling with types, Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, Available as Carnegie Mellon University School of Computer Science Technical Report CMU-CS-95-226, December 1995."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB10","unstructured":"G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, S. Zdancewic, TALx86: a realistic typed assembly language, Proc. 2nd Workshop on Compiler Support for System Software, Atlanta, Georgia, 1999, pp. 25\u201335."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB11","doi-asserted-by":"crossref","unstructured":"G. Morrisett, K. Crary, N. Glew, D. Walker, Stack-based typed assembly language, in: X. Leroy, A. Ohori (Eds.), Second Workshop on Types in Compilation, Lecture Notes in Computer Science, Vol. 1473, Springer, Kyoto, Japan, 1998, pp. 28\u201352, extended version published as CMU Technical Report CMU-CS-98-178.","DOI":"10.1007\/BFb0055511"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB12","unstructured":"G. Morrisett, D. Walker, K. Crary, N. Glew, From System F to typed assembly language, ACM Trans. Programming Language Systems 21 (3) (1999) 528\u2013569, an earlier version appeared in Proc. 25th Symp. on Principles of Programming Languages (POPL\u201998), San Diego, CA, 1998, pp. 85\u201397."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB13","series-title":"Conf. Record of the 24th Symposium on Principles of Programming Languages (POPL\u201997)","first-page":"106","article-title":"Proof-carrying code","author":"Necula","year":"1997"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB14","unstructured":"G.C. Necula, Compiling with proofs, Ph.D. Thesis, Carnegie Mellon University, available as Technical Report CMU-CS-98-154, October 1998."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB15","doi-asserted-by":"crossref","unstructured":"G. Necula, P. Lee, Safe kernel extensions without run-time checking, Proc. Second Symp. on Operating Systems Design and Implementation, Seattle, Washington, 1996, pp. 229\u2013243.","DOI":"10.1145\/238721.238781"},{"volume":"Vol. 1419","year":"1997","author":"Necula","key":"10.1016\/S0304-3975(01)00201-8_BIB16"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB17","doi-asserted-by":"crossref","unstructured":"G.C. Necula, P. Lee, Efficient representation and validation of logical proofs, Proc. 13th Annual Symp. on Logic in Computer Science (LICS\u201998), IEEE Computer Society Press, Indianapolis, Indiana, 1998, pp. 93\u2013104.","DOI":"10.1109\/LICS.1998.705646"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB18","series-title":"Proc. Conf. on Programming Language Design and Implementation (PLDI\u201998)","first-page":"333","article-title":"The design and implementation of a certifying compiler","author":"Necula","year":"1998"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB19","series-title":"Logical Frameworks","first-page":"149","article-title":"Logic programming in the LF logical framework","author":"Pfenning","year":"1991"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB20","doi-asserted-by":"crossref","unstructured":"F. Pfenning, Elf: A meta-language for deductive systems, in: A. Bundy (Ed.), Proc. 12th International Conf. on Automated Deduction, Springer, LNAI 814, Nancy, France, 1994, pp. 811\u2013815, system abstract.","DOI":"10.1007\/3-540-58156-1_66"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB21","doi-asserted-by":"crossref","unstructured":"F. Pfenning, Logical frameworks, in: A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, Chap. XXI, Elsevier Science and MIT Press, 2001, pp. 977\u20131061.","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB22","first-page":"179","article-title":"Algorithms for equality and unification in the presence of notational definitions","volume":"Vol. 1657","author":"Pfenning","year":"1998"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB23","doi-asserted-by":"crossref","unstructured":"F. Pfenning, C. Sch\u00fcrmann, System description: Twelf\u2014a meta-logical framework for deductive systems, in: H. Ganzinger (Ed.), Proc. 16th Internat. Conf. on Automated Deduction (CADE-16), Springer, LNAI 1632, Trento, Italy, 1999, pp. 202\u2013206.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB24","doi-asserted-by":"crossref","unstructured":"J.C. Reynolds, Definitional interpreters for higher-order programming languages, Proc. Conf. Record of the 25th National ACM Conference, Boston, 1972, pp. 717\u2013740.","DOI":"10.1145\/800194.805852"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB25","unstructured":"A. Stump, D.L. Dill, Generating proofs from a decision procedure, in: A. Pnueli, P. Traverso (Eds.), Proc. FLoC Workshop on Run-Time Result Verification, Trento, Italy, 1999."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB26","doi-asserted-by":"crossref","unstructured":"D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, P. Lee, TIL: a type-directed optimizing compiler for ML, ACM SIGPLAN Conf. on Programming Language Design and Implementation, Philadelphia, PA, 1996, pp. 181\u2013192.","DOI":"10.1145\/231379.231414"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB27","unstructured":"R. Virga, Higher-order rewriting with dependent types, Ph.D. Thesis, Department of Mathematical Sciences, Carnegie Mellon University, available as Technical Report CMU-CS-99-167, September 1999."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB28","doi-asserted-by":"crossref","unstructured":"R. Wahbe, S. Lucco, T. Anderson, S. Graham, Efficient software-based fault isolation, Proc. 14th ACM Symp. on Operating System Principles, 1993, pp. 203\u2013216.","DOI":"10.1145\/168619.168635"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB29","doi-asserted-by":"crossref","unstructured":"D. Walker, A type system for expressive security policies, Proc. 27th ACM Symp. on Principles of Programming Languages, Boston, MA, 2000, pp. 254\u2013267.","DOI":"10.1145\/325694.325728"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB30","unstructured":"H. Xi, R. Harper, A dependently typed assembly language, Technical Report OGI-CSE-99-008, Computer Science Department, Oregon Graduate Institute, July 1999."},{"key":"10.1016\/S0304-3975(01)00201-8_BIB31","series-title":"Proc. Conf. on Programming Language Design and Implementation (PLDI\u201998)","first-page":"249","article-title":"Eliminating array bound checking through dependent types","author":"Xi","year":"1998"},{"key":"10.1016\/S0304-3975(01)00201-8_BIB32","series-title":"Conf. Record of the 26th Symposium on Principles of Programming Languages (POPL\u201999)","first-page":"214","article-title":"Dependent types in practical programming","author":"Xi","year":"1999"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501002018?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501002018?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,11]],"date-time":"2024-12-11T00:14:48Z","timestamp":1733876088000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501002018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["S0304397501002018"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00201-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}