{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:13Z","timestamp":1781172313498,"version":"3.54.1"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319893655","type":"print"},{"value":"9783319893662","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89366-2_5","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T19:52:34Z","timestamp":1523649154000},"page":"91-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["A New Linear Logic for Deadlock-Free Session-Typed Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9927-7875","authenticated-orcid":false,"given":"Ornela","family":"Dardha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon J.","family":"Gay","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0304-3975(94)00103-0","volume":"135","author":"S Abramsky","year":"1994","unstructured":"Abramsky, S.: Proofs as processes. Theor. Comput. Sci. 135(1), 5\u20139 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-61455-2_10","volume-title":"Deductive Program Design","author":"Samson Abramsky","year":"1996","unstructured":"Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: Broy, M. (ed.) Proceedings of the NATO Advanced Study Institute on Deductive Program Design, pp. 35\u2013113 (1996)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BFb0014557","volume-title":"Theoretical Aspects of Computer Software","author":"S Abramsky","year":"1997","unstructured":"Abramsky, S., Gay, S., Nagarajan, R.: A type-theoretic approach to deadlock-freedom of asynchronous systems. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 295\u2013320. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0014557"},{"issue":"1\u20132","key":"5_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(98)00189-3","volume":"222","author":"S Abramsky","year":"1999","unstructured":"Abramsky, S., Gay, S.J., Nagarajan, R.: A specification structure for deadlock-freedom of synchronous processes. Theor. Comput. Sci. 222(1\u20132), 1\u201353 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-30936-1_2","volume-title":"A List of Successes That Can Change the World","author":"R Atkey","year":"2016","unstructured":"Atkey, R., Lindley, S., Morris, J.G.: Conflation confers concurrency. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 32\u201355. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_2"},{"issue":"ICFP","key":"5_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110281","volume":"1","author":"Stephanie Balzer","year":"2017","unstructured":"Balzer, S., Pfenning, F.: Manifest sharing with session types. In: Proceedings of the ACM on Programming Languages, vol. 1(ICFP), pp. 37:1\u201337:29 (2017)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"5_CR7","unstructured":"Barber, A.: Dual intuitionistic linear logic. Technical report ECS-LFCS-96-347, University of Edinburgh (1996). www.lfcs.inf.ed.ac.uk\/reports\/96\/ECS-LFCS-96-347"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G Bellin","year":"1994","unstructured":"Bellin, G., Scott, P.J.: On the pi-calculus and linear logic. Theor. Comput. Sci. 135(1), 11\u201365 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-540-85361-9_33","volume-title":"CONCUR 2008 - Concurrency Theory","author":"L Bettini","year":"2008","unstructured":"Bettini, L., Coppo, M., D\u2019Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418\u2013433. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_33"},{"key":"5_CR10","unstructured":"Br\u00e4uner, T.: Introduction to linear logic. Technical report BRICS LS-96-6, Basic Research Institute in Computer Science, University of Aarhus (1996)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-662-54434-1_9","volume-title":"Programming Languages and Systems","author":"L Caires","year":"2017","unstructured":"Caires, L., P\u00e9rez, J.A.: Linearity, control effects, and behavioral types. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 229\u2013259. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_9"},{"key":"5_CR12","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). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-662-43376-8_4","volume-title":"Coordination Models and Languages","author":"M Carbone","year":"2014","unstructured":"Carbone, M., Dardha, O., Montesi, F.: Progress as compositional lock-freedom. In: K\u00fchn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 49\u201364. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43376-8_4"},{"key":"5_CR14","unstructured":"Carbone, M., Lindley, S., Montesi, F., Sch\u00fcrmann, C., Wadler, P.: Coherence generalises duality: a logical explanation of multiparty session types. In: CONCUR. LIPIcs, vol. 59, pp. 33:1\u201333:15. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-72952-5_1","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M Coppo","year":"2007","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Yoshida, N.: Asynchronous session types and progress for object oriented languages. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 1\u201331. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72952-5_1"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Dardha, O.: Recursive session types revisited. In: BEAT. EPTCS, vol. 162, pp. 27\u201334 (2014)","DOI":"10.4204\/EPTCS.162.4"},{"key":"5_CR17","series-title":"Atlantis Studies in Computing","doi-asserted-by":"publisher","DOI":"10.2991\/978-94-6239-204-5","volume-title":"Type Systems for Distributed Programs: Components and Sessions","author":"O Dardha","year":"2016","unstructured":"Dardha, O.: Type Systems for Distributed Programs: Components and Sessions. Atlantis Studies in Computing, vol. 7. Atlantis Press, Paris (2016). https:\/\/doi.org\/10.2991\/978-94-6239-204-5"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session typed processes. In: 21st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2018 (Extended Version). http:\/\/www.dcs.gla.ac.uk\/~ornela\/publications\/DG18-Extended.pdf","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: PPDP, pp. 139\u2013150. ACM (2012)","DOI":"10.1145\/2370776.2370794"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Dardha, O., P\u00e9rez, J.A.: Comparing deadlock-free session typed processes. In: EXPRESS\/SOS. EPTCS, vol. 190, pp. 1\u201315 (2015)","DOI":"10.4204\/EPTCS.190.1"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-540-78663-4_18","volume-title":"Trustworthy Global Computing","author":"M Dezani-Ciancaglini","year":"2008","unstructured":"Dezani-Ciancaglini, M., de\u2019Liguoro, U., Yoshida, N.: On progress for structured communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 257\u2013275. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78663-4_18"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/11785477_20","volume-title":"ECOOP 2006 \u2013 Object-Oriented Programming","author":"M Dezani-Ciancaglini","year":"2006","unstructured":"Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session types for object-oriented languages. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 328\u2013352. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11785477_20"},{"issue":"1","key":"5_CR23","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":"5_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J Girard","year":"1987","unstructured":"Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR25","volume-title":"Proofs and Types","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/3-540-57208-2_35"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122\u2013138. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0053567"},{"key":"5_CR28","unstructured":"Kobayashi, N.: TyPiCal: type-based static analyzer for the pi-calculus. www-kb.is.s.u-tokyo.ac.jp\/~koba\/typical"},{"issue":"2","key":"5_CR29","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1145\/276393.278524","volume":"20","author":"N Kobayashi","year":"1998","unstructured":"Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Trans. Program. Lang. Syst. 20(2), 436\u2013482 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"5_CR30","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/S0890-5401(02)93171-8","volume":"177","author":"N Kobayashi","year":"2002","unstructured":"Kobayashi, N.: A type system for lock-free processes. Inf. Comput. 177(2), 122\u2013159 (2002)","journal-title":"Inf. Comput."},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-540-40007-3_26","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"N Kobayashi","year":"2003","unstructured":"Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 439\u2013453. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-40007-3_26"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/11817949_16","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"N Kobayashi","year":"2006","unstructured":"Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233\u2013247. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817949_16"},{"key":"5_CR33","unstructured":"Kobayashi, N.: Type systems for concurrent programs. Extended version of [31], Tohoku University (2007)"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/978-3-662-46669-8_23","volume-title":"Programming Languages and Systems","author":"S Lindley","year":"2015","unstructured":"Lindley, S., Morris, J.G.: A semantics for propositions as sessions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 560\u2013584. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_23"},{"key":"5_CR35","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Padovani, L.: From lock freedom to progress using session types. In: PLACES. EPTCS, vol. 137, pp. 3\u201319 (2013)","DOI":"10.4204\/EPTCS.137.2"},{"key":"5_CR37","doi-asserted-by":"crossref","unstructured":"Padovani, L.: Deadlock and lock freedom in the linear $$\\pi $$\u03c0-Calculus. In: CSL-LICS, pp. 72:1\u201372:10. ACM (2014)","DOI":"10.1145\/2603088.2603116"},{"key":"5_CR38","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., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398\u2013413. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58184-7_118"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP, pp. 161\u2013172. ACM (2011)","DOI":"10.1145\/2003476.2003499"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-38493-6_17","volume-title":"Coordination Models and Languages","author":"H Torres Vieira","year":"2013","unstructured":"Torres Vieira, H., Thudichum Vasconcelos, V.: Typing progress in communication-centred systems. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 236\u2013250. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38493-6_17"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as sessions. In: ICFP, pp. 273\u2013286. ACM (2012)","DOI":"10.1145\/2364527.2364568"},{"issue":"12","key":"5_CR42","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2699407","volume":"58","author":"P Wadler","year":"2015","unstructured":"Wadler, P.: Propositions as types. Commun. ACM 58(12), 75\u201384 (2015)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89366-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:20:52Z","timestamp":1571156452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89366-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893655","9783319893662"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89366-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}