{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:08Z","timestamp":1725494288869},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755951"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75596-8_1","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T14:03:37Z","timestamp":1194098617000},"page":"1-14","source":"Crossref","is-referenced-by-count":0,"title":["Policies and Proofs for Code Auditing"],"prefix":"10.1007","author":[{"given":"Nathan","family":"Whitehead","sequence":"first","affiliation":[]},{"given":"Jordan","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Mart\u00edn","family":"Abadi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"706","DOI":"10.1145\/155183.155225","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems\u00a015(4), 706\u2013734 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"issue":"2\/3","key":"1_CR3","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076(2\/3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"De Treville, J.: Binder, a logic-based security language. In: Proceedings of the 2002 IEEE Symposium on Security and Privacy, pp. 105\u2013113 (2002)","DOI":"10.1109\/SECPRI.2002.1004365"},{"key":"1_CR5","unstructured":"ECMA. C# and common language infrastructure standards (2007), Online at \n                    \n                      http:\/\/msdn2.microsoft.com\/en-us\/netframework\/aa569283.aspx"},{"key":"1_CR6","unstructured":"Perl Foundation. Perl 5.8.8 documentation: perlsec - Perl security, Online at \n                    \n                      http:\/\/perldoc.perl.org\/perlsec.html"},{"issue":"1","key":"1_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"issue":"4","key":"1_CR8","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/138873.138874","volume":"10","author":"B. Lampson","year":"1992","unstructured":"Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems\u00a010(4), 265\u2013310 (1992)","journal-title":"ACM Transactions on Computer Systems"},{"key":"1_CR9","volume-title":"The JavaTM Virtual Machine Specification","author":"T. Lindholm","year":"1997","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification. Addison-Wesley, Reading (1997)"},{"issue":"3","key":"1_CR10","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems\u00a021(3), 528\u2013569 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"1_CR12","unstructured":"Microsoft\u00a0Developer Network. About ActiveX controls,(2007), Online at \n                    \n                      http:\/\/msdn2.microsoft.com\/en-us\/library\/Aa751971.aspx"},{"issue":"6","key":"1_CR13","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1017\/S0956796897002906","volume":"7","author":"P. \u00d8rb\u00e6k","year":"1997","unstructured":"\u00d8rb\u00e6k, P., Palsberg, J.: Trust in the \u03bb-calculus. Journal of Functional Programming\u00a07(6), 557\u2013591 (1997)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"1_CR15","unstructured":"Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. In: CSFW 2005. Proceedings of the 18th IEEE Workshop on Computer Security Foundations, pp. 255\u2013269 (2005)"},{"key":"1_CR16","unstructured":"The Coq\u00a0Development Team. The Coq proof assistant, \n                    \n                      http:\/\/coq.inria.fr\/"},{"key":"1_CR17","unstructured":"Whitehead, N.: Towards static analysis in a logic for code authorization. (Manuscript)"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-540-74464-1_17","volume-title":"TYPES 2006","author":"N. Whitehead","year":"2007","unstructured":"Whitehead, N.: A certified distributed security logic for authorizing code. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 253\u2013268. Springer, Heidelberg (2007)"},{"key":"1_CR19","series-title":"Lecture Notes in Artificial Intelligence","first-page":"110","volume-title":"LPAR 2004","author":"N. Whitehead","year":"2005","unstructured":"Whitehead, N., Abadi, M.: BCiC: A system for code authentication and verification. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 110\u2013124. Springer, Heidelberg (2005)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Whitehead, N., Abadi, M., Necula, G.: By reason and authority: A system for authorization of proof-carrying code. In: CSFW 2004. Proceedings of the 17th IEEE Computer Security Foundations Workshop, pp. 236\u2013250 (2004)","DOI":"10.1109\/CSFW.2004.1310744"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:25:19Z","timestamp":1619519119000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755951"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_1","relation":{},"subject":[]}}