{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:53Z","timestamp":1761611213799,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540416357"},{"type":"electronic","value":"9783540445777"}],"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"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44577-3_6","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T18:23:39Z","timestamp":1181413419000},"page":"86-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":50,"title":["A Language-Based Approach to Security"],"prefix":"10.1007","author":[{"given":"Fred B.","family":"Schneider","sequence":"first","affiliation":[]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,29]]},"reference":[{"issue":"4","key":"6_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters 21(4):181\u2013185, Oct. 1985.","journal-title":"Information Processing Letters"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"B. Bershad, S. Savage, P. Pardyak, E. Sirer, M. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility, safety and performance in the SPIN operating system. In Proc. 15th ACM Symp. on Operating System Principles (SOSP), pages 267\u2013284, Copper Mountain, Dec. 1995.","DOI":"10.1145\/224057.224077"},{"key":"6_CR3","unstructured":"R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, 1986."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"D. Engler, M. Kaashoek, and J. O\u2019Toole. Exokernel: An operating system architecture for application-level resource management. In Proc. 15th ACM Symp. on Operating System Principles (SOSP), Copper Mountain, 1995.","DOI":"10.1145\/224056.224076"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"U. Erlingsson and F. B. Schneider. SASI enforcement of security policies: A retrospective. In Proceedings of the New Security Paradigms Workshop, Ontario, Canada, Sept. 1999.","DOI":"10.1145\/335169.335201"},{"key":"6_CR6","unstructured":"U. Erlingsson and F. B. Schneider. IRM enforcement of java stack inspection. In IEEE Symposium on Security and Privacy, Oakland, California, May 2000."},{"issue":"1","key":"6_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A fram ework for defining logics. Journal of the ACM, 40(1):143\u2013184, Jan. 1993.","journal-title":"Journal of the ACM"},{"issue":"2","key":"6_CR8","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness ofm ultiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125\u2013143, March 1977.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR9","series-title":"Lect Notes Comput Sci","first-page":"119","volume-title":"Distributed Systems-Methods and Tools for Specification","author":"L. Lamport","year":"1985","unstructured":"L. Lamport. Logical Foundation. In Distributed Systems-Methods and Tools for Specification, pages 119\u2013130, Lecture Notes in Computer Science, Vol 190. M. Paul and H.J. Siegert, editors. Springer-Verlag, 1985, New York."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"J. McLean. A general theory ofc omposition for trace sets closed under selective interleaving functions. In Proc. 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 79\u201393, Oakland, Calif., May 1994.","DOI":"10.1109\/RISP.1994.296590"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), pages 85\u201397, San Diego California, USA, January 1998.","DOI":"10.1145\/268946.268954"},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528\u2013569, May 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"G. C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings of Operating System Design and Implementation, pages 229\u2013243, Seattle, Oct. 1996.","DOI":"10.1145\/248155.238781"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Programming Languages (POPL), pages 106\u2013119, Jan. 1997.","DOI":"10.1145\/263699.263712"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"J. Saltzer and M. Schroeder. The protection ofi nformation in computer systems. Proceedings of the IEEE, 9(63), Sept. 1975.","DOI":"10.1109\/PROC.1975.9939"},{"volume-title":"Trust in Cyberspace","year":"1999","key":"6_CR16","unstructured":"F. B. Schneider, editor. Trust in Cyberspace. National Academy Press, Washington, D.C., 1999."},{"key":"6_CR17","unstructured":"F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 2(4), Mar. 2000."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"M. Seltzer, Y. Endo, C. Small, and K. Smith. Dealing with disaster: Surviving misbehaved kernel extensions. In Proc. USENIX Symp. on Operating Systems Design and Implementation (OSDI), pages 213\u2013227, Seattle, Washington, Oct. 1996.","DOI":"10.1145\/248155.238779"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A typedirected optimizing compiler for ML. In ACM Conf. on Programming Language Design and Implementation, pages 181\u2013192, Philadelphia, May 1996.","DOI":"10.1145\/249069.231414"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Efficient software-based fault isolation. In Proc. 14th ACM Symp. on Operating System Principles (SOSP), pages 203\u2013216, Asheville, Dec. 1993.","DOI":"10.1145\/173668.168635"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 249\u2013257, Montreal Canada, June 1998.","DOI":"10.1145\/277652.277732"},{"key":"6_CR22","unstructured":"E. Yasuhiro, J. Gwertzman, M. Seltzer, C. Small, K.A. Smith, and D. Tang. VINO: The 1994 fall harvest. Technical Report TR-34-94, Harvard Computer Center for Research in Computing Technology, 1994."}],"container-title":["Lecture Notes in Computer Science","Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44577-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T04:35:01Z","timestamp":1737088501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44577-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540416357","9783540445777"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44577-3_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"29 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}