{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T21:18:46Z","timestamp":1725743926060},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642404467"},{"type":"electronic","value":"9783642404474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40447-4_3","type":"book-chapter","created":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T01:00:39Z","timestamp":1375750839000},"page":"37-52","source":"Crossref","is-referenced-by-count":1,"title":["The Blame Theorem for a Linear Lambda Calculus with Type Dynamic"],"prefix":"10.1007","author":[{"given":"Luminous","family":"Fennell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/103135.103138","volume":"13","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Pierce, B., Plotkin, G.: Dynamic typing in a statically typed language. ACM TOPLAS\u00a013(2), 237\u2013268 (1991)","journal-title":"ACM TOPLAS"},{"issue":"1&2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S.: Computational interpretations of linear logic. Theor. Comput. Sci\u00a0111(1&2), 3\u201357 (1993)","journal-title":"Theor. Comput. Sci"},{"issue":"11-13","key":"3_CR3","doi-asserted-by":"publisher","first-page":"1484","DOI":"10.1016\/j.tcs.2009.11.014","volume":"411","author":"S. Alves","year":"2010","unstructured":"Alves, S., Fern\u00e1ndez, M., Florido, M., Mackie, I.: G\u00f6del\u2019s system T revisited. Theoretical Computer Science\u00a0411(11-13), 1484\u20131500 (2010)","journal-title":"Theoretical Computer Science"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"Typed Lambda Calculi and Applications","author":"P.N. Benton","year":"1993","unstructured":"Benton, P.N., Bierman, G.M., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 75\u201390. Springer, Heidelberg (1993)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-14107-2_5","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"G. Bierman","year":"2010","unstructured":"Bierman, G., Meijer, E., Torgersen, M.: Adding dynamic types to C#. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 76\u2013100. Springer, Heidelberg (2010)"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/S1571-0661(04)80874-0","volume":"41","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M., Pitts, A.M., Russo, C.V.: Operational properties of Lily, a polymorphic linear lambda calculus with recursion. Electr. Notes Theor. Comput. Sci.\u00a041(3), 70\u201388 (2000)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L. Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 222\u2013236. Springer, Heidelberg (2010)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of the 18th ESOP","year":"2009","unstructured":"Castagna, G. (ed.): ESOP 2009. LNCS, vol.\u00a05502. Springer, Heidelberg (2009)"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/0167-6423(94)00004-2","volume":"22","author":"F. Henglein","year":"1994","unstructured":"Henglein, F.: Dynamic typing: Syntax and proof theory. Science of Computer Programming\u00a022, 197\u2013230 (1994)","journal-title":"Science of Computer Programming"},{"key":"3_CR11","unstructured":"Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. In: Trends in Functional Programming (TFP) (2007)"},{"key":"3_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1498926.1498930","volume":"31","author":"J. Matthews","year":"2009","unstructured":"Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. ACM TOPLAS\u00a031, 12:1\u201312:44 (2009)","journal-title":"ACM TOPLAS"},{"key":"3_CR13","unstructured":"Palsberg, J. (ed.): Proc. 37th ACM Symp. POPL, Madrid, Spain. ACM Press (January 2010)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73589-2_2","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"J.G. Siek","year":"2007","unstructured":"Siek, J.G., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 2\u201327. Springer, Heidelberg (2007)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Siek, J.G., Garcia, R., Taha, W.: Exploring the design space of higher-order casts. In: Castagna [8], pp. 17\u201331","DOI":"10.1007\/978-3-642-00590-9_2"},{"key":"3_CR16","unstructured":"Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional Programming Workshop (September 2006)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Siek, J.G., Wadler, P.: Threesomes, with and without blame. In: Palsberg [13], pp. 365\u2013376","DOI":"10.1145\/1707801.1706342"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/3-540-58184-7_118","volume-title":"PARLE \u201994 Parallel Architectures and Languages Europe","author":"K. Takeuchi","year":"1994","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol.\u00a0817, pp. 398\u2013413. Springer, Heidelberg (1994)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/978-3-642-11957-6_29","volume-title":"Programming Languages and Systems","author":"J.A. Tov","year":"2010","unstructured":"Tov, J.A., Pucella, R.: Stateful contracts for affine types. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 550\u2013569. Springer, Heidelberg (2010)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Tov, J.A., Pucella, R.: Practical affine types. In: Proc.\u00a038th ACM Symp. POPL, Austin, TX, USA, pp. 447\u2013458. ACM Press (January 2011)","DOI":"10.1145\/1926385.1926436"},{"issue":"1-2","key":"3_CR21","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0304-3975(99)00054-7","volume":"227","author":"D.N. Turner","year":"1999","unstructured":"Turner, D.N., Wadler, P.: Operational interpretations of linear logic. Theoretical Computer Science\u00a0227(1-2), 231\u2013248 (1999)","journal-title":"Theoretical Computer Science"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Wadler, P., Findler, R.B.: Well-typed programs can\u2019t be blamed. In: Castagna [8], pp. 1\u201316","DOI":"10.1007\/978-3-642-00590-9_1"},{"issue":"1","key":"3_CR23","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A. Wright","year":"1994","unstructured":"Wright, A., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Wrigstad, T., Nardelli, F.Z., Lebresne, S., \u00d6stlund, J., Vitek, J.: Integrating typed and untyped code in a scripting language. In: Palsberg [13], pp. 377\u2013388","DOI":"10.1145\/1707801.1706343"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40447-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T12:36:37Z","timestamp":1558010197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40447-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642404467","9783642404474"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40447-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}