{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:59:13Z","timestamp":1742385553900,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664086"},{"type":"electronic","value":"9783540483403"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48340-3_26","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T17:04:52Z","timestamp":1184605492000},"page":"284-298","source":"Crossref","is-referenced-by-count":21,"title":["Language-Based Security"],"prefix":"10.1007","author":[{"given":"Dexter","family":"Kozen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and R. Stata. A type system for Java bytecode subroutines. In Proc. 25th Symp. Principles of Programming Languages, pages 149\u2013160. ACM SIG-PLAN\/SIGACT, January 1998.","DOI":"10.1145\/268946.268959"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"B. Bershad, S. Savage, P. Pardyak, E. G. Sirer, D. Becker, M. Fiuczynski, C. Chambers, and S. Eggers. Extensibility, safety, and performance in the SPIN operating system. In Proc. 15th Symp. Operating System Principles, pages 267\u2013284. ACM, December 1995.","DOI":"10.1145\/224056.224077"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th Symp. Principles of Programming Languages, pages 262\u2013275. ACM SIGPLAN\/SIGACT, January 1999.","DOI":"10.1145\/292540.292564"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Drew Dean, Ed Felten, and Dan Wallach. JAVA security: From HotJava to Netscape and beyond. In Proc. Symp. Security and Privacy. IEEE, May 1996.","DOI":"10.1109\/SECPRI.1996.502681"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Whitfield Diffie and Susan Landau. Privacy on the Line: The Politics of Wiretapping and Encryption. MIT Press, 1998.","DOI":"10.7551\/mitpress\/5571.001.0001"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Ulfar Erlingsson and Fred B. Schneider. SASI enforcement of security policies: A retrospective, April 1999. Preprint.","DOI":"10.1145\/335169.335201"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"N. Glew and G. Morrisett. Type-safe linking and modular assembly language. In Proc. 26th Symp. Principles of Programming Languages, pages 250\u2013261. ACM SIGPLAN\/SIGACT, January 1999.","DOI":"10.1145\/292540.292563"},{"issue":"1","key":"26_CR8","doi-asserted-by":"crossref","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. J. Assoc. Comput. Mach., 40(1):143\u2013184, January 1993.","journal-title":"J. Assoc. Comput. Mach."},{"key":"26_CR9","unstructured":"Luke Hornof and Trevor Jim. Certifying compilation and run-time code generation. In Proc. Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 60\u201374. ACM, January 1999."},{"key":"26_CR10","unstructured":"Bill Joy and Ken Kennedy, co-chairs. Information Technology Research: Investing in Our Future. President\u2019s Information Technology Advisory Committee, February 1999. http:\/\/www.ccic.gov\/ ."},{"key":"26_CR11","unstructured":"Dexter Kozen. Efficient code certification. Technical Report 98-1661, Computer Science Department, Cornell University, January 1998."},{"key":"26_CR12","unstructured":"Tim Lindholm and Frank Yellin. The JAVA virtual machine specification. Addison Wesley, 1996."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Proc. Workshop on Compiler Support for System Software, pages 25\u201335. ACM SIGPLAN, May 1999.","DOI":"10.21236\/ADA358572"},{"key":"26_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Proc. Workshop on Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In Xavier Leroy and Atsushi Ohori, editors, Proc. Workshop on Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28\u201352. Springer-Verlag, March 1998."},{"key":"26_CR15","unstructured":"G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL\/ML compiler: Performance and safety through types. In 1996 Workshop on Compiler Support for Systems Software, 1996."},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In 25th ACM SIGPLAN\/SIGSIGACT Symposium on Principles of Programming Languages, pages 85\u201397, San Diego California, USA, January 1998.","DOI":"10.1145\/268946.268954"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Andrew C. Myers. JFlow: Practical static information flow control. In Proc. 26th Symp. Principles of Programming Languages. ACM, January 1999.","DOI":"10.1145\/292540.292561"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Andrew C. Myers and Barbara Liskov. A decentralized model for information flow control. In Proc. 16th Symp. Operating System Principles, pages 129\u2013142. ACM, October 1997.","DOI":"10.1145\/269005.266669"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Andrew C. Myers and Barbara Liskov. Complete, safe information flow with decentralized labels. In Proc. Symp. Security and Privacy, pages 186\u2013197. IEEE, May 1998.","DOI":"10.1109\/SECPRI.1998.674834"},{"key":"26_CR20","unstructured":"National Coordination Office for Computing, Information, and Communications. Information Technology for the 21st Century: A Bold Investment in America\u2019s Future, 24 January 1999. Draft. http:\/\/www.ccic.gov\/ ."},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"George C. Necula. Proof-carrying code. In Proc. 24th Symp. Principles of Programming Languages, pages 106\u2013119. ACM SIGPLAN\/SIGACT, January 1997.","DOI":"10.1145\/263699.263712"},{"key":"26_CR22","unstructured":"George C. Necula. Compiling with proofs. PhD thesis, Carnegie Mellon University, September 1998."},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proc. 2nd Symp. Operating System Design and Implementation. ACM, October 1996.","DOI":"10.1145\/238721.238781"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Proc. Conf. Programming Language Design and Implementation, pages 333\u2013344. ACM SIGPLAN, 1998.","DOI":"10.1145\/277652.277752"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Efficient representation and validation of proofs. In Proc. 13th Symp. Logic in Computer Science, pages 93\u2013104. IEEE, June 1998.","DOI":"10.1109\/LICS.1998.705646"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Safe, untrusted agents using using proof-carrying code. In Giovanni Vigna, editor, Special Issue on Mobile Agent Security, volume 1419 of Lect. Notes in Computer Science, pages 61\u201391. Springer-Verlag, June 1998.","DOI":"10.1007\/3-540-68671-1_5"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Robert O\u2019Callahan. A simple, comprehensive type system for Java bytecode subroutines. In Proc. 26th Symp. Principles of Programming Languages, pages 70\u201378. ACM SIGPLAN\/SIGACT, January 1999.","DOI":"10.1145\/292540.292549"},{"key":"26_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0028319","volume-title":"Proc. 11th Int. Workshop WDAG\u2019 97","author":"F. B. Schneider","year":"1997","unstructured":"Fred B. Schneider. Towards fault-tolerant and secure agentry. In Proc. 11th Int. Workshop WDAG\u2019 97, volume 1320 of Lecture Notes in Computer Science, pages 1\u201314. ACM SIGPLAN, Springer-Verlag, September 1997."},{"key":"26_CR29","unstructured":"Fred B. Schneider. Enforceable security policies. Technical Report TR98-1664, Computer Science Department, Cornell University, January 1998."},{"key":"26_CR30","unstructured":"Fred B. Schneider, editor. Trust in Cyberspace. Committee on Information Systems Trustworthiness, Computer Science and Telecommunications Board, National Research Council. National Academy Press, 1999."},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In Conf. Programming Language Design and Implementation. ACM SIGPLAN, 1996.","DOI":"10.1145\/231379.231414"},{"key":"26_CR32","doi-asserted-by":"crossref","unstructured":"R. Wahbe, S. Lucco, T. E. Anderson, and S. L Graham. Efficient software-based fault isolation. In Proc. 14th Symp. Operating System Principles, pages 203\u2013216. ACM, December 1993.","DOI":"10.1145\/168619.168635"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"David Walker. A type system for expressive security policies. In Proc. FLOC\u201999 Workshop on Run-time Result Verification, July 1999. To appear.","DOI":"10.1145\/325694.325728"},{"key":"26_CR34","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Proc. Conf. Programming Language Design and Implementation, pages 249\u2013257. ACM SIGPLAN, June 1998.","DOI":"10.1145\/277650.277732"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48340-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:15:22Z","timestamp":1737288922000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48340-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664086","9783540483403"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-48340-3_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}