{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:05:34Z","timestamp":1767236734999,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662459164"},{"type":"electronic","value":"9783662459171"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45917-1_10","type":"book-chapter","created":{"date-parts":[[2014,12,22]],"date-time":"2014-12-22T14:34:17Z","timestamp":1419258857000},"page":"144-158","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Session Types with Gradual Typing"],"prefix":"10.1007","author":[{"given":"Peter","family":"Thiemann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,12,23]]},"reference":[{"key":"10_CR1","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. 6269, pp. 222\u2013236. Springer, Heidelberg (2010)"},{"issue":"5","key":"10_CR2","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1016\/j.ic.2008.03.028","volume":"207","author":"M Dezani-Ciancaglini","year":"2009","unstructured":"Dezani-Ciancaglini, M., Drossopoulou, S., Mostrous, D., Yoshida, N.: Objects and session types. Information and Computation 207(5), 595\u2013641 (2009)","journal-title":"Information and Computation"},{"key":"10_CR3","unstructured":"Disney, T., Flanagan, C.: Gradual information flow typing. In: STOP (2011)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-40447-4_3","volume-title":"Trends in Functional Programming","author":"L Fennell","year":"2013","unstructured":"Fennell, L., Thiemann, P.: The blame theorem for a linear lambda calculus with type dynamic. In: Loidl, H.-W., Pe\u00f1a, R. (eds.) TFP 2012. LNCS, vol. 7829, pp. 37\u201352. Springer, Heidelberg (2013)"},{"key":"10_CR5","first-page":"224","volume-title":"CSF","author":"L Fennell","year":"2013","unstructured":"Fennell, L., Thiemann, P.: Gradual security typing with references. In: Cortier, V., Datta, A. (eds.) CSF, pp. 224\u2013239. IEEE, New Orleans (2013)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49099-X_6","volume-title":"Programming Languages and Systems","author":"SJ Gay","year":"1999","unstructured":"Gay, S.J., Hole, M.: Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74\u201390. Springer, Heidelberg (1999)"},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"SJ Gay","year":"2010","unstructured":"Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010)","journal-title":"J. Funct. Program."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Vasconcelos, V.T., Ravara, A., Gesbert, N., Caldeira, A. Z.: Modular session types for distributed object-oriented programming. In: POPL 2010 [15], pp. 299\u2013312","DOI":"10.1145\/1707801.1706335"},{"key":"10_CR9","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 22, 197\u2013230 (1994)","journal-title":"Science of Computer Programming"},{"key":"10_CR10","unstructured":"Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. In: Trends in Functional Programming (TFP) (2007)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR 1993","author":"K Honda","year":"1993","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509\u2013523. Springer, Heidelberg (1993)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-19056-8_4","volume-title":"Distributed Computing and Internet Technology","author":"K Honda","year":"2011","unstructured":"Honda, K., Mukhamedov, A., Brown, G., Chen, T.-C., Yoshida, N.: Scribbling interactions with a formal foundation. In: Natarajan, R., Ojo, A. (eds.) ICDCIT 2011. LNCS, vol. 6536, pp. 55\u201375. Springer, Heidelberg (2011)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Wadler, P. (eds.) Proc. 35th ACM Symp. POPL, pp. 273\u2013284. ACM Press, San Francisco (2008)","DOI":"10.1145\/1328438.1328472"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-40787-1_8","volume-title":"Runtime Verification","author":"R Hu","year":"2013","unstructured":"Hu, R., Neykova, R., Yoshida, N., Demangeon, R., Honda, K.: Practical interruptible conversations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 130\u2013148. Springer, Heidelberg (2013)"},{"key":"10_CR15","unstructured":"Proc. 37th ACM Symp. POPL. ACM Press, Madrid (January 2010)"},{"key":"10_CR16","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":"JG Siek","year":"2007","unstructured":"Siek, J.G., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2\u201327. Springer, Heidelberg (2007)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Siek, J.G., Wadler, P.: Threesomes, with and without blame. In: POPL 2010 [15], pp. 365\u2013376","DOI":"10.1145\/1707801.1706342"},{"key":"10_CR18","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":"JA Tov","year":"2010","unstructured":"Tov, J.A., Pucella, R.: Stateful contracts for affine types. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 550\u2013569. Springer, Heidelberg (2010)"},{"issue":"1\u20132","key":"10_CR19","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.tcs.2006.06.028","volume":"368","author":"VT Vasconcelos","year":"2006","unstructured":"Vasconcelos, V.T., Ravara, A., Gay, S.J.: Type checking a multithreaded functional language with session types. Theoretical Computer Science 368(1\u20132), 64\u201387 (2006)","journal-title":"Theoretical Computer Science"},{"key":"10_CR20","first-page":"273","volume-title":"ICFP 2012","author":"P Wadler","year":"2012","unstructured":"Wadler, P.: Propositions as sessions. In: Findler, R.B. (ed.) ICFP 2012, pp. 273\u2013286. ACM, Copenhagen, Denmark (2012)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00590-9_1","volume-title":"Programming Languages and Systems","author":"P Wadler","year":"2009","unstructured":"Wadler, P., Findler, R.B.: Well-typed programs can\u2019t be blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1\u201316. Springer, Heidelberg (2009)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-22655-7_22","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"R Wolff","year":"2011","unstructured":"Wolff, R., Garcia, R., Tanter, \u00c9., Aldrich, J.: Gradual typestate. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 459\u2013483. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45917-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T05:12:11Z","timestamp":1676005931000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-45917-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662459164","9783662459171"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45917-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"23 December 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}