{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T09:10:01Z","timestamp":1737364201795,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_3","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"31-46","source":"Crossref","is-referenced-by-count":9,"title":["Temporal Logic for Proof-Carrying Code"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Bernard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 243\u2013253, Boston, MA, January 2000.","DOI":"10.1145\/325694.325727"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Andrew Bernard and Peter Lee. Temporal logic for proof-carrying code. Technical Report CMU-CS-02-130, Carnegie Mellon University, School of Computer Science, 2002. In preparation.","DOI":"10.1007\/3-540-45620-1_3"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. In Proceedings of the ACM SIG-PLAN\u2019 00 conference on programming language design and implementation, pages 95\u2013107, Vancouver, BC Canada, June 2000.","DOI":"10.1145\/349299.349315"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262\u2013275, San Antonio, TX, January 1999.","DOI":"10.1145\/292540.292564"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Karl Crary and Stephnie Weirich. Resource bound certification. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 184\u2013198, Boston, MA, January 2000.","DOI":"10.1145\/325694.325716"},{"key":"3_CR6","unstructured":"\u00dalfar Erlingsson and Fred B. Schneider. IRM enforcement of Java stack inspection. In RSP: 21th IEEE Computer Society Symposium on Research in Security and Privacy, 2000."},{"key":"3_CR7","unstructured":"Dexter Kozen. Efficient code certification. Technical Report TR98-1661, Cornell University, Computer Science Department, January 1998."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Neophytos G. Michael and Andrew W. Appel. Machine instruction syntax and semantics in higher order logic. In Proceedings of the 17th International Conference on Automated Deduction (CADE-17), June 2000.","DOI":"10.1007\/10721959_2"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85\u201397, San Diego, CA, January 1998.","DOI":"10.1145\/268946.268954"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106\u2013119, Paris, France, January 1997.","DOI":"10.1145\/263699.263712"},{"key":"3_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68671-1_5","volume-title":"Mobile Agents and Security","author":"G. C. Necula","year":"1998","unstructured":"George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In Mobile Agents and Security, volume 1419 of Lecture Notes in Computer Science. Springer Verlag, 1998."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"George C. Necula and S. P. Rahul. Oracle-based checking of untrusted software. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 142\u2013154, London, UK, January 2001.","DOI":"10.1145\/360204.360216"},{"key":"3_CR14","unstructured":"George Ciprian Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998. Available as Technical Report CMU-CS-98-154."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. System description: Twelf \u2014 A meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202\u2013206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"3_CR16","unstructured":"Fred B. Schneider. Enforceable security policies. Technical Report TR99-1759, Cornell University, Computer Science Department, July 1999."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. Efficient software-based fault isolation. In Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles, pages 203\u2013216, Asheville, NC, December 1993.","DOI":"10.1145\/168619.168635"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"David Walker. A type system for expressive security policies. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 254\u2013267, Boston, MA, January 2000.","DOI":"10.1145\/325694.325728"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:52:19Z","timestamp":1737363139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}