{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:23Z","timestamp":1725564563392},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_2","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"2-15","source":"Crossref","is-referenced-by-count":16,"title":["Security Types Preserving Compilation"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Amitabh","family":"Basu","sequence":"additional","affiliation":[]},{"given":"Tamara","family":"Rezk","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1\u20134","key":"2_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/176454.176456","volume":"2","author":"T. Ball","year":"1993","unstructured":"Ball, T.: What\u2019s in a region? Or computing control dependence regions in nearlinear time for reducible control flow. ACM Letters on Programming Languages and Systems\u00a02(1\u20134), 1\u201316 (1993)","journal-title":"ACM Letters on Programming Languages and Systems"},{"key":"2_CR2","volume-title":"Proceedings of CSFW 2002","author":"A. Banerjee","year":"2002","unstructured":"Banerjee, A., Naumann, D.A.: Secure Information Flow and Pointer Confinement in a Java-like Language. In: Proceedings of CSFW 2002, IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10705424_4","volume-title":"Functional and Logic Programming","author":"G. Barthe","year":"1999","unstructured":"Barthe, G., Serpette, B.: Partial evaluation and non-interference for object calculi. In: Middeldorp, A. (ed.) FLOPS 1999. LNCS, vol.\u00a01722, pp. 53\u201367. Springer, Heidelberg (1999)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47813-2_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C. Bernardeschi","year":"2002","unstructured":"Bernardeschi, C., De Francesco, N.: Combining Abstract Interpretation and Model Checking for analysing Security Properties of Java Bytecode. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 1\u201315. Springer, Heidelberg (2002)"},{"key":"2_CR5","doi-asserted-by":"crossref","first-page":"369","DOI":"10.3233\/JCS-2002-10404","volume":"10","author":"P. Bieber","year":"2002","unstructured":"Bieber, P., Cazin, J., Wiels, V., Zanon, G., Girard, P., Lanet, J.-L.: Checking Secure Interactions of Smart Card Applets: Extended version. Journal of Computer Security\u00a010, 369\u2013398 (2002)","journal-title":"Journal of Computer Security"},{"unstructured":"Coglio, A.: Simple Verification Technique for Complex Java Bytecode Subroutines. In: Proceedings of FTFJP 2002 (2002)","key":"2_CR6"},{"key":"2_CR7","first-page":"11","volume-title":"Proceedings of SOSP 1982","author":"J. Goguen","year":"1982","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: Proceedings of SOSP 1982, pp. 11\u201322. IEEE Computer Society, Los Alamitos (1982)"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/268946.268976","volume-title":"Proceedings of POPL 1998","author":"N. Heintze","year":"1998","unstructured":"Heintze, N., Riecke, J.: The SLam calculus: programming with secrecy and integrity. In: Proceedings of POPL 1998, pp. 365\u2013377. ACM Press, New York (1998)"},{"key":"2_CR9","first-page":"81","volume-title":"Proceedings of POPL 2002","author":"K. Honda","year":"2002","unstructured":"Honda, K., Yoshida, N.: A Uniform Type Structure for Secure Information Flow. In: Proceedings of POPL 2002, pp. 81\u201392. ACM Press, New York (2002)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-36579-6_8","volume-title":"Compiler Construction","author":"C. League","year":"2003","unstructured":"League, C., Shao, Z., Trifonov, V.: Precision in Practice: A Type-Preserving Java Compiler. In: Hedin, G. (ed.) CC 2003. LNCS, vol.\u00a02622, pp. 106\u2013120. Springer, Heidelberg (2003)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Computer Aided Verification","author":"X. Leroy","year":"2001","unstructured":"Leroy, X.: Java bytecode verification: an overview. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 265\u2013285. Springer, Heidelberg (2001)"},{"key":"2_CR12","first-page":"228","volume-title":"Proceedings of POPL 1999","author":"A.C. Myers","year":"1999","unstructured":"Myers, A.C.: Jflow: Practical mostly-static information flow control. In: Proceedings of POPL 1999, pp. 228\u2013241. ACM Press, New York (1999)"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-Carrying Code. In: Proceedings of POPL 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Proceedings of PLDI 1998, pp. 333\u2013344 (1998)","key":"2_CR14","DOI":"10.1145\/277652.277752"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F. Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems\u00a025(1), 117\u2013158 (2003)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR16","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.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Comunications\u00a021, 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Comunications"},{"unstructured":"Simonet, V.: Fine-grained Information Flow Analysis for a Lambda-Calculus with Sum Types. In: Proceedings of CSFW 2002, pp. 223\u2013237 (2002)","key":"2_CR17"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"D. Volpano","year":"1997","unstructured":"Volpano, D., Smith, G.: A Type-Based Approach to Program Security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 607\u2013621. Springer, Heidelberg (1997)"},{"key":"2_CR19","first-page":"156","volume-title":"Proceedings of CSFW 1997","author":"D. Volpano","year":"1997","unstructured":"Volpano, D., Smith, G.: Eliminating covert flows with minimum typings. In: Proceedings of CSFW 1997, pp. 156\u2013168. IEEE Press, Los Alamitos (1997)"},{"doi-asserted-by":"crossref","unstructured":"Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security, 167\u2013187 (December 1996)","key":"2_CR20","DOI":"10.3233\/JCS-1996-42-304"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-45309-1_4","volume-title":"Programming Languages and Systems","author":"S. Zdancewic","year":"2001","unstructured":"Zdancewic, S., Myers, A.: Secure information flow and CPS. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 46\u201361. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T17:40:41Z","timestamp":1559583641000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}