{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:30:00Z","timestamp":1743096600348,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417392"},{"type":"electronic","value":"9783540447160"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44716-4_2","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T18:16:34Z","timestamp":1187201794000},"page":"21-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Scalable Architecture for Proof-Carrying Code"],"prefix":"10.1007","author":[{"given":"George C.","family":"Necula","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,21]]},"reference":[{"issue":"5","key":"2_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/358438.349315","volume":"35","author":"C. Colby","year":"2000","unstructured":"Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. ACM SIGPLAN Notices, 35(5):95\u2013107, May 2000.","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. De Bruijn","year":"1972","unstructured":"N. DeBruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Mat., 34:381\u2013392, 1972.","journal-title":"Indag. Mat."},{"issue":"1","key":"2_CR3","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"2_CR4","first-page":"527","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527\u2013568, May 1999.","journal-title":"From system F to typed assembly language"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"George C. Necula. Proof-carrying code. In The 24th Annual ACM Symposium on Principles of Programming Languages, pages 106\u2013119. ACM, January 1997.","DOI":"10.1145\/263699.263712"},{"key":"2_CR6","unstructured":"George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998. Also available as CMU-CS-98-154."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Safe kernel extensions without runtime checking. In Second Symposium on Operating Systems Design and Implementations, pages 229\u2013243. Usenix, October 1996.","DOI":"10.1145\/248155.238781"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Efficient representation and validation of proofs. In Thirteenth Annual Symposium on Logic in Computer Science, pages 93\u2013104, Indianapolis, June 1998. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1998.705646"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"George C. Necula and Shree P. Rahul. Oracle-based checking of untrusted programs. In The 28th Annual ACM Symposium on Principles of Programming Languages. ACM, January 2001. To appear.","DOI":"10.1145\/360204.360216"},{"issue":"2","key":"2_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0743-1066(94)00016-Y","volume":"23","author":"R. Ramesh","year":"1995","unstructured":"R. Ramesh, I. V. Ramakrishnan, and David Scott Warren. Automatadriven indexing of Prolog clauses. Journal of Logic Programming, 23(2):151\u2013202, May 1995.","journal-title":"Journal of Logic Programming"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44716-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T10:54:45Z","timestamp":1737370485000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44716-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417392","9783540447160"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-44716-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"21 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}